PRuning Through Satisfaction
PRuning Through Satisfaction
复制标题
通过满意度进行修剪
DOI：
10.1007/978-3-319-70389-3_12
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Armin Biere
中科院分区：
文献类型：
--
作者：
Marijn J. H. Heule;B. Kiesl;M. Seidl;Armin Biere
解决命题逻辑可满足性问题的经典方法是从搜索空间中删除不可满足的分支。我们通过删除某些分支来进行更激进的修剪，这些分支存在其他更令人满意的分支。这是通过扩展流行的冲突驱动子句学习（CDCL）范式与所谓的\（\mathsf {PR}\）-子句学习。我们在SAT求解器Lingeling中实现了我们的新范式，称为满意度驱动的小句学习（SDCL）。著名的鸽子洞公式的实验表明，我们的方法可以自动产生证明的不可满足性，其大小是立方的鸽子，而普通的CDCL求解器只能产生证明的指数大小。
The classical approach to solving the satisfiability problem of propositional logic prunes unsatisfiable branches from the search space. We prune more agressively by also removing certain branches for which there exist other branches that are more satisfiable. This is achieved by extending the popular conflict-driven clause learning (CDCL) paradigm with so-called \(\mathsf {PR}\) -clause learning. We implemented our new paradigm, named satisfaction-driven clause learning (SDCL), in the SAT solver Lingeling. Experiments on the well-known pigeon hole formulas show that our method can automatically produce proofs of unsatisfiability whose size is cubic in the number of pigeons while plain CDCL solvers can only produce proofs of exponential size.