Document Open Access Logo

An Exponential Separation Between Deterministic CDCL and DPLL Solvers

Authors Sahil Samar , Marc Vinyals , Vijay Ganesh

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.30.pdf
  • Filesize: 0.96 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • SAT solvers
  • CDCL
  • Proof Systems
  • VSIDS

Metrics

Abstract

We prove that there exists a deterministic configuration of Conflict-Driven Clause Learning (CDCL) SAT solvers using a variant of the VSIDS branching heuristic that solves instances of the Ordering Principle (OP) CNF formulas in time polynomial in n, where n is the number of variables in such formulas. Since tree-like resolution is known to have an exponential lower bound for proof size for OP formulas, it follows that CDCL under this configuration has an exponential separation with any solver that is polynomially equivalent to tree-like resolution and therefore any configuration of DPLL SAT solvers.

Cite As Get BibTex

Sahil Samar, Marc Vinyals, and Vijay Ganesh. An Exponential Separation Between Deterministic CDCL and DPLL Solvers. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.30

Author Details

Sahil Samar
  • School of Computer Science, Georgia Institute of Technology, Atlanta, GA, USA
Marc Vinyals
  • School of Computer Science, University of Auckland, New Zealand
Vijay Ganesh
  • School of Computer Science, Georgia Institute of Technology, Atlanta, GA, USA

Acknowledgements

We would like to thank Vincent Liew for his help in verifying the work in this paper. Additionally, we want to thank the anonymous reviewers for their valuable feedback.

References

  1. Michael Alekhnovich, Jan Johannsen, Toniann Pitassi, and Alasdair Urquhart. An exponential separation between regular and general resolution. Theory of Computing, 3(1):81-102, 2007. URL: https://doi.org/10.4086/toc.2007.v003a005.
  2. Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res., 40:353-373, 2011. URL: https://doi.org/10.1613/jair.3152.
  3. Albert Atserias and Moritz Müller. Automating resolution is NP-Hard. J. ACM, 67(5):31:1-31:17, 2020. URL: https://doi.org/10.1145/3409472.
  4. Gilles Audemard and Laurent Simon. Experimenting with small changes in conflict-driven clause learning algorithms. In International Conference on Principles and Practice of Constraint Programming, pages 630-634. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85958-1_55.
  5. Armin Biere and Andreas Fröhlich. Evaluating CDCL variable scoring schemes. In Marijn Heule and Sean A. Weaver, editors, Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, volume 9340 of Lecture Notes in Computer Science, pages 405-422. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_29.
  6. Maria Luisa Bonet and Nicola Galesi. Optimality of size-width tradeoffs for resolution. Comput. Complex., 10(4):261-276, 2001. URL: https://doi.org/10.1007/s000370100000.
  7. Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. On interpolation and automatization for Frege systems. SIAM J. Comput., 29(6):1939-1967, 2000. URL: https://doi.org/10.1137/S0097539798353230.
  8. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  9. Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, Jakob Nordström, and Laurent Simon. Seeking practical CDCL insights from theoretical sat benchmarks. In IJCAI, volume 18, pages 1300-1308, 2018. URL: https://doi.org/10.24963/ijcai.2018/181.
  10. Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard, Jakob Nordström, and Marc Vinyals. Trade-offs between time and memory in a tighter model of CDCL SAT solvers. In International Conference on Theory and Applications of Satisfiability Testing, pages 160-176. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_11.
  11. Vijay Ganesh and Moshe Y. Vardi. On the unreasonable effectiveness of SAT solvers. In Tim Roughgarden, editor, Beyond the Worst-Case Analysis of Algorithms, pages 547-566. Cambridge University Press, 2020. URL: https://doi.org/10.1017/9781108637435.032.
  12. Hadi Katebi, Karem A. Sakallah, and João P. Marques Silva. Empirical study of the anatomy of modern sat solvers. In Karem A. Sakallah and Laurent Simon, editors, Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings, volume 6695 of Lecture Notes in Computer Science, pages 343-356. Springer, Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21581-0_27.
  13. Balakrishnan Krishnamurthy. Short proofs for tricky formulas. Acta informatica, 22(3):253-275, 1985. URL: https://doi.org/10.1007/BF00265682.
  14. Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Exponential recency weighted average branching heuristic for SAT solvers. In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (AAAI-16), pages 689-695, 2016. URL: https://doi.org/10.1609/aaai.v30i1.10439.
  15. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001, pages 530-535. ACM, 2001. URL: https://doi.org/10.1145/378239.379017.
  16. Nathan Mull, Shuo Pang, and Alexander A. Razborov. On CDCL-based proof systems with the ordered decision strategy. SIAM J. Comput., 51(4):1368-1399, 2022. URL: https://doi.org/10.1137/20m1362528.
  17. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers with restarts. In Ian P. Gent, editor, Principles and Practice of Constraint Programming - CP 2009, 15th International Conference, CP 2009, Lisbon, Portugal, September 20-24, 2009, Proceedings, volume 5732 of Lecture Notes in Computer Science, pages 654-668. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04244-7_51.
  18. Lawrence Ryan. Efficient algorithms for clause-learning SAT solvers. Master’s thesis, Simon Fraser University, 2004. Google Scholar
  19. Sahil Samar, Marc Vinyals, and Vijay Ganesh. An exponential separation between deterministic CDCL and DPLL solvers. CoRR, abs/2603.16156, 2026. URL: https://doi.org/10.48550/arXiv.2603.16156.
  20. João P. Marques Silva and Karem A. Sakallah. GRASP - a new search algorithm for satisfiability. In Rob A. Rutenbar and Ralph H. J. M. Otten, editors, Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1996, San Jose, CA, USA, November 10-14, 1996, pages 220-227. IEEE, IEEE Computer Society / ACM, 1996. URL: https://doi.org/10.1109/ICCAD.1996.569607.
  21. Gunnar Stålmarck. Short resolution proofs for a sequence of tricky formulas. Acta Informatica, 33(3):277-280, 1996. URL: https://doi.org/10.1007/s002360050044.
  22. Marc Vinyals. Hard examples for common variable decision heuristics. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pages 1652-1659. AAAI Press, 2020. URL: https://doi.org/10.1609/aaai.v34i02.5527.
  23. Marc Vinyals. Textbooksat. https://github.com/marcvinyals/textbooksat, 2026. Accessed: 2026-05-10.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact