Speaker: Marijn Heule

Title: PRuning Through Satisfaction

Abstract:

The classical approach to solving the satisfiability problem of
propositional logic prunes unsatisfiable branches from the search
space. We prune more aggressively 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.