[Zurück]

M. Heule, B. Kiesl, M. Seidl, A. Biere:
"PRuning Through Satisfaction";
Vortrag: 13th International Haifa Verification Conference (HVC 2017), Haifa, Israel; 13.11.2017 - 15.11.2017; in: "Proceedings of the 13th Haifa Verification Conference", Lecture Notes in Computer Science / Springer, 10629 / Cham (2017), ISBN: 978-3-319-70388-6; S. 179 - 194.

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 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.

SAT solving, propositional logic, conflict-driven clause learning, CDCL

http://dx.doi.org/10.1007/978-3-319-70389-3_12

http://publik.tuwien.ac.at/files/publik_266903.pdf