Generating Extended Resolution Proofs with a BDD-Based SAT Solver
Generating Extended Resolution Proofs with a BDD-Based SAT Solver
复制标题
使用基于 BDD 的 SAT 求解器生成扩展分辨率证明
DOI：
10.1145/3595295
复制
发表时间：
2023
影响因子：
0.5
通讯作者：
Heule, Marijn J.
中科院分区：
文献类型：
--
作者：
Bryant, Randal E.;Heule, Marijn J.
2006年，Biere、Jussila和Sinz提出了一个关键的观察结果，即构建简化有序二叉决策图(BDDS)的算法背后的基本逻辑可以编码为扩展分辨率逻辑框架中的证明步骤。通过这一点，基于BDD的布尔可满足性(SAT)求解器可以生成可检查的不可满足性证明。这样的证明表明，如果用户不信任BDD包或构建在其上的SAT解算器，该公式确实是不可满足的。我们扩展了他们的工作，以实现公式变量的任意存在量化，这是基于BDD的SAT解算器的关键功能。我们通过扩展现有的BDD包实现的基于BDD的求解器对几个具有挑战性的布尔可满足性问题进行了演示，从而证明了该方法的有效性。我们的结果展示了奇偶公式以及Urquhart、残缺棋盘和鸽子问题的可伸缩性，远远超过了其他生成证明的SAT解算器。
In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in theextended resolutionlogical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability. Such a proof indicates that the formula is truly unsatisfiable without requiring the user to trust the BDD package or the SAT solver built on top of it.We extend their work to enable arbitrary existential quantification of the formula variables, a critical capability for BDD-based SAT solvers. We demonstrate the utility of this approach by applying a BDD-based solver, implemented by extending an existing BDD package, to several challenging Boolean satisfiability problems. Our results demonstrate scaling for parity formulas as well as the Urquhart, mutilated chessboard, and pigeonhole problems far beyond that of other proof-generating SAT solvers.
登录
查看更多内容
通过满意度进行修剪
DOI：
10.1007/978-3-319-70389-3_12
发表时间：
2017
期刊：
ArXiv
影响因子：
--
作者：
Marijn J. H. Heule;B. Kiesl;M. Seidl;Armin Biere
通讯作者：
Armin Biere
DOI：
10.1007/978-3-030-51825-7_1
发表时间：
2020-06-26
期刊：
Theory and Applications of Satisfiability Testing – SAT 2020
影响因子：
--
作者：
Chew L;Heule MJ
通讯作者：
Heule MJ
使用高斯约当消元法生成 CDCL 求解器的证明
DOI：
10.48550/arxiv.2304.04292
发表时间：
2023
期刊：
ArXiv
影响因子：
--
作者：
M. Soos;R. Bryant
通讯作者：
R. Bryant
伪布尔推理的子句证明
DOI：
10.1007/978-3-030-99524-9_25
发表时间：
2022
期刊：
International Conference on Tools and Algorithms for the Construction and Analysis of Systems
影响因子：
--
作者：
Bryant, Randal E.;Heule, Marijn J.
通讯作者：
Heule, Marijn J.
影响因子：
1.2
作者：
A. V. Gelder
通讯作者：
A. V. Gelder