Abstract
Over the last decades Boolean satisfiability (SAT) solvers based on
conflict-driven clause learning (CDCL) have developed to the point
where they can handle formulas with millions of variables. Yet a
deeper understanding of how these solvers can be so successful has
remained elusive. In this work we shed light on CDCL performance by
using theoretical benchmarks, which have the attractive features of
being a) scalable, b) extremal with respect to different proof search
parameters, and c) theoretically easy in the sense of having short
proofs in the resolution proof system underlying CDCL. This allows for
a systematic study of solver heuristics and how efficiently they
search for proofs. We report results from extensive experiments on a
wide range of benchmarks. Our findings include several examples where
theory predicts and explains CDCL behaviour, but also raise a number
of intriguing questions for further study.
Keywords
- Constraints and SAT: SAT
- Constraints and SAT: SAT: Evaluation and Analysis
- Constraints and SAT: SAT: Solvers and Tools
