Running time of CDCL compared to DPLL

Question

What's the complexity of Conflict-Driven Clause Learning SAT solvers, compared to DPLL solvers? Was it proven that CDCL is faster in general? Are there instances of SAT that are hard for CDCL but easy for DPLL?

Answer 1

Both CDCL and DPLL need exponential time in the worst case. I am not sure if it can be proved that CDCL is always faster than DPLL on every instance, but there is major empirical data suggesting it dominates. For a nice, short overview see the presentation Boolean Satisfiability Solving: Past, Present & Future by Joao Marques-Silva. He also has quite a few related talks online, see here.

CDCL is the dominating solver among all modern solvers. I would claim CDCL does indeed always dominate, and that is because it's basically a DPLL-based procedure, but with additional enhancements. It uses information gained during the search, restart strategies, special data structures, and so on.

There are instances that make all the known DPLL-like algorithms run in exponential time. For example, Alekhnovich et al. [1] exhibit such a family of 3-SAT instances. For more information on satisfiability, both theoretical and practical, I think one of the best sources are the Handbook of Satisfiability [2] and the regular International Conferences on Theory and Applications of Satisfiability Testing, known as SAT.

---

[1] Alekhnovich, M., Hirsch, E., and Itykson, D. Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. JAR, 35(1-3), 51-72, 2005.

[2] Biere, A., Heule, M., van Maaren, H. and Walsh, T. (Eds.). Handbook of Satisfiability. IOS Press, 2009.