Johan Frisk: On the Power of Conflict-Driven Clause-Learning SAT Solvers

I will present two theoretical results on modern SAT solvers regarding their power as proof systems compared to general resolution. We will see that a formalization of the algorithm used by conflict-driven clause learning (CDCL) SAT solvers polynomially simulates general resolution assuming that a specific decision strategy is used. Earlier proofs of this required an extra preprocessing step on the input formula or modifications to the solver that do not correspond to how CDCL solvers work in practical implementations.

In contrast to the first result, which works only under a non-deterministic perfect-choice decision strategy, our second result shows that with a probability of 50% the same solvers, now equipped with a totally random decision strategy, end up behaving like width-k resolution after O(n^2k+1) conflicts and restarts.

The results are from the two articles:

• "On the Power of Clause-Learning SAT Solvers with Restarts" by Knot Pipatsrisawat and Adnan Darwiche (CP 2009).
• "Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution" by Albert Atserias, Johannes Klaus Fichte and Marc Thurley (SAT 2009).

This is a presentation of the theoretical part of my Master's degree project.

The first part of the seminar will be a self-contained 45-minute overview of the two papers. After a break, those who so wish can return for a somewhat more detailed discussion of some of the proofs.