AAAIDec, 2020

关于连续的基于本地 BDD 的混合 SAT 求解

PDF
TL;DR提出一种基于连续局部搜索与信念传播结合的算法 GradSAT，能在求解混合布尔约束问题方面有很好的应用表现，对称布尔约束和小系数伪布尔约束也可适用，并有望成为解决布尔满足性和优化问题的有效方法之一。
continuous local searchboolean constraintsgradsatmaxsatoptimization problems
发现论文，激发创造
  • 基于 GPU 的混合 SAT 求解的大规模并行连续局部搜索

    提出了基于梯度驱动连续局部搜索（CLS）的高度并行混合 SAT 求解器 FastFourierSAT，该算法利用图形处理单元（GPU）的并行性能加速计算，可以比之前的方法快 100 + 倍，并在更大规模的案例上表现出良好的性能。

    Aug, 2023

  • 重新思考 MaxSAT 局部搜索求解器中的软冲突伪布尔约束

    本研究使用 MaxSAT 问题中的 SPB 约束和子句权重技术，提出了一种新的局部搜索算法 SPB-MaxSAT，为 MaxSAT 局部搜索求解器的子句权重方法提供了新的视角和优秀的性能。

    Jan, 2024

  • FourierSAT: 一个基于傅里叶展开的代数框架求解混合布尔约束问题

    FourierSAT 是一种基于布尔函数的傅里叶分析的不完全的 SAT 求解器，其提出一种用于解决具有不同类型限制的系统的代数框架，并通过实验证明在某些基准测试上，它比其他解算器更具鲁棒性。

    Dec, 2019

  • 利用深度学习构建带性能界限的随机局部搜索 SAT 求解器

    利用图神经网络训练适用于布尔可满足性问题的 SLS 求解器，可显著提高性能，平均解决比例更高、步骤更少，具有性能保证。

    Sep, 2023

  • NLocalSAT: 利用解预测提升局部搜索

    本文介绍了一种结合 solution prediction model 和神经网络的方法 ——NLocalSAT，用于提高 stochastic local search 在解 Boolean satisfiability problem 时的有效性，并且在 SAT Competition 2018 的实验中取得了 27% ~ 62% 的性能提升。

    Jan, 2020

  • 挑战 SAT 求解中分辨率限制

    本文提出了一种新的问题转化方法，将 CNF 公式的决策问题转化为 Horn 公式的最大可满足性问题，并证明了在鸽笼公式的情况下 MaxSAT resolution steps 的数量存在多项式绑定。

    May, 2017

  • 认识与利用子句学习的潜力

    本文通过分析阐述了布尔可满足性问题中，采用了子句学习增强 DPLL 的实现方式是最高效的，并与已有的分辨规则证明体系相对照，证明了该方法在一些条件下可以提供更短的证明过程，且该算法可以通过利用问题结构，通过导向学习算法的方法取得指数性的加速。

    Jun, 2011

  • DeciLS-PBO: 一种有效的伪布尔优化局部搜索方法

    本文通过两种方法提高局部搜索算法的效率解决了伪布尔优化问题 (PBO)。首先使用一些机制 (如单位传播) 将其广义化为 PBO 问题，然后利用措辞这个桥梁来增强对其的理解。实验表明我们的算法比现有算法性能更好。

    Jan, 2023

  • 驱动 CDCL 搜索

    通过嵌入特定领域的启发式方法来提高 CDCL 算法的性能并不容易，本文提出了一种通用框架来设计和实现新的启发式方法，并在两个工业领域实验中取得成功。

    Nov, 2016

  • 利用因果推理解释 SAT 求解

    本文介绍了使用因果推理探究 SAT 求解器内在工作机制的方法 CausalSAT，并通过实验验证了其中四条经验法则和三个与现代 SAT 求解器实现密切相关的问题。

    Jun, 2023