Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

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?

share|improve this question
add comment

1 Answer

up vote 4 down vote accepted

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.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.