Talks and Poster Presentations (with Proceedings-Entry):
M. Heule, B. Kiesl, M. Seidl, A. Biere:
"PRuning Through Satisfaction";
Talk: 13th International Haifa Verification Conference (HVC 2017),
Haifa, Israel;
11-13-2017
- 11-15-2017; in: "Proceedings of the 13th Haifa Verification Conference",
Lecture Notes in Computer Science / Springer,
10629 / Cham
(2017),
ISBN: 978-3-319-70388-6;
179
- 194.
English abstract:
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.
Keywords:
SAT solving, propositional logic, conflict-driven clause learning, CDCL
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-319-70389-3_12
Electronic version of the publication:
http://publik.tuwien.ac.at/files/publik_266903.pdf
Created from the Publication Database of the Vienna University of Technology.