论文标题
在连续的本地BDD搜索混合动力SAT解决
On Continuous Local BDD-Based Search for Hybrid SAT Solving
论文作者
论文摘要
我们通过提出一种新的方法来找到布尔限制的混合系统，探索SAT解决中连续局部搜索（CL）的潜力。该算法基于CLS与二进制决策图（BDD）的信念传播相结合。我们的框架接受了承认紧凑型BDD的所有布尔限制，包括对称的布尔限制和小型伪树状限制作为有趣的家庭。我们提出了一种新型算法，用于有效地计算CLS所需的梯度。我们通过将其应用于许多基准实例，研究多功能CLS求解器Gradsat的功能和局限性。实验结果表明，Gradsat可能是现有SAT和MAXSAT求解器组合的有用补充，以解决布尔值的满意度和优化问题。
We explore the potential of continuous local search (CLS) in SAT solving by proposing a novel approach for finding a solution of a hybrid system of Boolean constraints. The algorithm is based on CLS combined with belief propagation on binary decision diagrams (BDDs). Our framework accepts all Boolean constraints that admit compact BDDs, including symmetric Boolean constraints and small-coefficient pseudo-Boolean constraints as interesting families. We propose a novel algorithm for efficiently computing the gradient needed by CLS. We study the capabilities and limitations of our versatile CLS solver, GradSAT, by applying it on many benchmark instances. The experimental results indicate that GradSAT can be a useful addition to the portfolio of existing SAT and MaxSAT solvers for solving Boolean satisfiability and optimization problems.
