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.
CITATION STYLE
Heule, M. J. H., Kiesl, B., Seidl, M., & Biere, A. (2017). PRuning through satisfaction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10629 LNCS, pp. 179–194). Springer Verlag. https://doi.org/10.1007/978-3-319-70389-3_12
Mendeley helps you to discover research relevant for your work.