Gustav Sennton: Towards an understanding of the power of CDCL SAT solvers

The Boolean satisfiability problem (SAT) is the canonical NP-complete problem and hence it seems natural to expect that solving instances of the SAT problem is difficult. However, in practice conflict-driven clause learning (CDCL) SAT solvers do well on many large-scale real-world instances. Therefore it is interesting to study the strengths and weaknesses of CDCL solvers.

CDCL solvers implicitly find resolution proofs for unsatisfiable formulas, but how small are such proofs compared to the smallest possible resolution proof? It was recently shown that CDCL solvers can produce proofs of size at most polynomially longer than the smallest resolution proof. However, these results are non-constructive, i.e. the algorithm is non-deterministic. When it comes to constructive results it was recently shown that, with high probability, the running time of a CDCL solver is polynomial in the size of the smallest corresponding resolution proof as long as the clauses in the resolution proof have constant size (and given certain theoretical assumptions about the CDCL model).

In the first half of this seminar I will go over the resolution proof system, explain how a CDCL solver works, and then give an overview of how to prove guarantees for CDCL performance in terms of resolution. During the second half of the seminar we will look at some of the proofs in more detail.

The seminar is based on the following two articles:

Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution from 2011 by Atserias, Fichte and Thurley dx.doi.org/10.1613/jair.3152

On the power of clause-learning SAT solvers as resolution engines from 2011 by Pipatsrisawat and Darwiche dx.doi.org/10.1016/j.artint.2010.10.002