Document Open Access Logo

Limits of CDCL Learning via Merge Resolution

Authors Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova, Vijay Ganesh

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.27.pdf
  • Filesize: 0.65 MB
  • 19 pages

Document Identifiers

Author Details

Marc Vinyals
  • University of Auckland, New Zealand
Chunxiao Li
  • University of Waterloo, Canada
Noah Fleming
  • Memorial University of Newfoundland, St. John’s, Canada
Antonina Kolokolova
  • Memorial University of Newfoundland, St. John’s, Canada
Vijay Ganesh
  • University of Waterloo, Canada

Acknowledgements

The authors are grateful to Yuval Filmus and a long list of participants in the program Satisfiability: Theory, Practice, and Beyond at the Simons Institute for the Theory of Computing for numerous discussions. We also thank the SAT 2023 reviewers for their helpful suggestions. This work was done in part while the authors were visiting the Simons Institute for the Theory of Computing.

Cite AsGet BibTex

Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova, and Vijay Ganesh. Limits of CDCL Learning via Merge Resolution. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.27

Abstract

In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. However, previous work does not address the tightness of the simulation, i.e., the question of how large this overhead needs to be. In this paper, we address this question by focusing on an important property of proofs generated by CDCL solvers that employ standard learning schemes, namely that the derivation of a learned clause has at least one inference where a literal appears in both premises (aka, a merge literal). Specifically, we show that proofs of this kind can simulate resolution proofs with at most a linear overhead, but there also exist formulas where such overhead is necessary or, more precisely, that there exist formulas with resolution proofs of linear length that require quadratic CDCL proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Constraint and logic programming
Keywords
  • proof complexity
  • resolution
  • merge resolution
  • CDCL
  • learning scheme

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Peter B. Andrews. Resolution with merging. J. ACM, 15(3):367-381, 1968. Google Scholar
  2. Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. Journal of Artificial Intelligence Research, 40:353-373, January 2011. Preliminary version in SAT '09. Google Scholar
  3. Gilles Audemard, Lucas Bordeaux, Youssef Hamadi, Saïd Jabbour, and Lakhdar Sais. A generalized framework for conflict analysis. In Hans Kleine Büning and Xishun Zhao, editors, Theory and Applications of Satisfiability Testing - SAT 2008, 11th International Conference, SAT 2008, Guangzhou, China, May 12-15, 2008. Proceedings, volume 4996 of Lecture Notes in Computer Science, pages 21-27. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-79719-7_3.
  4. Roberto J. Bayardo Jr. and Robert Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the 14th National Conference on Artificial Intelligence (AAAI '97), pages 203-208, July 1997. Google Scholar
  5. Paul Beame, Henry Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research, 22:319-351, December 2004. Preliminary version in IJCAI '03. Google Scholar
  6. Olaf Beyersdorff and Benjamin Böhm. Understanding the relative strength of QBF CDCL solvers and QBF resolution. In James R. Lee, editor, 12th Innovations in Theoretical Computer Science Conference, ITCS 2021, January 6-8, 2021, Virtual Conference, volume 185 of LIPIcs, pages 12:1-12:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITCS.2021.12.
  7. Avrim L Blum and Merrick L Furst. Fast planning through planning graph analysis. Artificial intelligence, 90(1-2):281-300, 1997. Google Scholar
  8. Sam Buss and Jakob Nordström. Proof complexity and SAT solving. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, chapter 7, pages 233-350. IOS Press, 2nd edition, 2021. URL: https://doi.org/10.3233/FAIA200990.
  9. Samuel R. Buss, Jan Hoffmann, and Jan Johannsen. Resolution trees with lemmas: Resolution refinements that characterize DLL-algorithms with clause learning. Logical Methods in Computer Science, 4(4:13), December 2008. Google Scholar
  10. Cristian Cadar, Vijay Ganesh, Peter M Pawlowski, David L Dill, and Dawson R Engler. EXE: Automatically Generating Inputs of Death. ACM Transactions on Information and System Security (TISSEC), 12(2):1-38, 2008. Google Scholar
  11. Alvaro del Val. Tractable databases: How to make propositional unit resolution complete through compilation. In Jon Doyle, Erik Sandewall, and Pietro Torasso, editors, Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning (KR'94). Bonn, Germany, May 24-27, 1994, pages 551-561. Morgan Kaufmann, 1994. Google Scholar
  12. Nachum Dershowitz, Ziyad Hanna, and Alexander Nadel. Towards a better understanding of the functionality of a conflict-driven SAT solver. In João Marques-Silva and Karem A. Sakallah, editors, Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings, volume 4501 of Lecture Notes in Computer Science, pages 287-293. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-72788-0_27.
  13. Julian Dolby, Mandana Vaziri, and Frank Tip. Finding Bugs Efficiently With a SAT Solver. In Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 195-204, 2007. URL: https://doi.org/10.1145/1287624.1287653.
  14. Nick Feng and Fahiem Bacchus. Clause size reduction with all-uip learning. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 28-45. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_3.
  15. Philipp Hertel, Fahiem Bacchus, Toniann Pitassi, and Allen Van Gelder. Clause learning can effectively P-simulate general propositional resolution. In Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI '08), pages 283-290, July 2008. Google Scholar
  16. Chunxiao Li, Noah Fleming, Marc Vinyals, Toniann Pitassi, and Vijay Ganesh. Towards a complexity-theoretic understanding of restarts in sat solvers. In Theory and Applications of Satisfiability Testing-SAT 2020: 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings 23, pages 233-249. Springer, 2020. Google Scholar
  17. João Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 133-182. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200987.
  18. João P. Marques-Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506-521, May 1999. Preliminary version in ICCAD '96. Google Scholar
  19. Burkhard Monien and Ewald Speckenmeyer. Solving satisfiability in less than 2ⁿ steps. Discret. Appl. Math., 10(3):287-295, 1985. URL: https://doi.org/10.1016/0166-218X(85)90050-2.
  20. 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 '01), pages 530-535, June 2001. Google Scholar
  21. Nathan Mull, Shuo Pang, and Alexander A. Razborov. On CDCL-based proof systems with the ordered decision strategy. In Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT '20), volume 12178 of Lecture Notes in Computer Science, pages 149-165. Springer, July 2020. Google Scholar
  22. Knot Pipatsrisawat and Adnan Darwiche. A new clause learning scheme for efficient unsatisfiability proofs. In Dieter Fox and Carla P. Gomes, editors, Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17, 2008, pages 1481-1484. AAAI Press, 2008. URL: http://www.aaai.org/Library/AAAI/2008/aaai08-243.php.
  23. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence, 175(2):512-525, February 2011. Preliminary version in CP '09. Google Scholar
  24. Lawrence Ryan. Efficient algorithms for clause-learning SAT solvers. Master’s thesis, Simon Fraser University, 2004. Google Scholar
  25. Niklas Sörensson and Armin Biere. Minimizing learned clauses. In Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT '09), volume 5584 of Lecture Notes in Computer Science, pages 237-243. Springer, July 2009. Google Scholar
  26. Allen Van Gelder. Pool resolution and its relation to regular resolution and DPLL with clause learning. In Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '05), volume 3835 of Lecture Notes in Computer Science, pages 580-594. Springer, 2005. Google Scholar
  27. Marc Vinyals. Hard examples for common variable decision heuristics. In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI '20), pages 1652-1659, February 2020. Google Scholar
  28. Yichen Xie and Alexander Aiken. Saturn: A SAT-Based Tool for Bug Detection. In Proceedings of the 17th International Conference on Computer Aided Verification, CAV 2005, pages 139-143, 2005. URL: https://doi.org/10.1007/11513988_13.
  29. Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, and Sharad Malik. Efficient conflict driven learning in Boolean satisfiability solver. In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD '01), pages 279-285, November 2001. Google Scholar
  30. Edward Zulkoski, Ruben Martins, Christoph M. Wintersteiger, Jia Hui Liang, Krzysztof Czarnecki, and Vijay Ganesh. The effect of structural measures and merges on SAT solver performance. In John N. Hooker, editor, Principles and Practice of Constraint Programming - 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings, volume 11008 of Lecture Notes in Computer Science, pages 436-452. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98334-9_29.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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