Trimming while checking clausal proofs
Trimming while checking clausal proofs
复制标题
在检查子句证明时进行修剪
DOI：
10.1109/fmcad.2013.6679408
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Nathan Wetzler
中科院分区：
文献类型：
--
作者：
Marijn J. H. Heule;W. Hunt;Nathan Wetzler
可满足性求解器可以产生多个可满足性结果;它们还可以产生子句证明、分解证明、不可满足核和克雷格插值。这些额外的结果可能需要对求解器进行大量修改，特别是如果使用预处理和处理中技术;然而，CDCL求解器可以很容易地以非常低的开销发出子句证明。我们提出了一种新的方法与相关的工具，有效地验证子句证明，并可以提取额外的结果子句证明。我们的工具架构可以很容易地从任何CDCL求解器获得这样的结果。实验评估表明，我们的工具可以验证子句证明比现有的工具更快。此外，与改进的SAT求解器相比，附加结果的质量（如不可满足的核心）更高。
Conflict-driven clause learning (CDCL) satisfiability solvers can emit more than a satisfiability result; they can also emit clausal proofs, resolution proofs, unsatisfiable cores, and Craig interpolants. Such additional results may require substantial modifications to a solver, especially if preprocessing and inprocessing techniques are used; however, CDCL solvers can easily emit clausal proofs with very low overhead. We present a new approach with an associated tool that efficiently validates clausal proofs and can distill additional results from clausal proofs. Our tool architecture makes it easy to obtain such results from any CDCL solver. Experimental evaluation shows that our tool can validate clausal proofs faster than existing tools. Additionally, the quality of the additional results, such as unsatisfiable cores, is higher when compared to modified SAT solvers.