Document Open Access Logo

QCDCL vs QBF Resolution: Further Insights

Authors Benjamin Böhm , Olaf Beyersdorff

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.4.pdf
  • Filesize: 0.94 MB
  • 17 pages

Document Identifiers

Author Details

Benjamin Böhm
  • Friedrich-Schiller-Universität Jena, Germany
Olaf Beyersdorff
  • Friedrich-Schiller-Universität Jena, Germany

Funding

  • Beyersdorff, Olaf: Carl-Zeiss Foundation and DFG grant BE 4209/3-1.

Cite As Get BibTex

Benjamin Böhm and Olaf Beyersdorff. QCDCL vs QBF Resolution: Further Insights. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.SAT.2023.4

Abstract

We continue the investigation on the relations of QCDCL and QBF resolution systems. In particular, we introduce QCDCL versions that tightly characterise QU-Resolution and (a slight variant of) long-distance Q-Resolution. We show that most QCDCL variants - parameterised by different policies for decisions, unit propagations and reductions - lead to incomparable systems for almost all choices of these policies.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • QBF
  • CDCL
  • resolution
  • proof complexity
  • simulations
  • lower bounds

Metrics

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

Related Versions

References

  1. 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. Google Scholar
  2. Albert Atserias and Moritz Müller. Automating resolution is NP-hard. In IEEE Annual Symposium on Foundations of Computer Science (FOCS), pages 498-509. IEEE Computer Society, 2019. Google Scholar
  3. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Form. Methods Syst. Des., 41(1):45-65, 2012. Google Scholar
  4. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In Proc. Theory and Applications of Satisfiability Testing (SAT), pages 154-169, 2014. Google Scholar
  5. Paul Beame, Henry A. Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR), 22:319-351, 2004. URL: https://doi.org/10.1613/jair.1410.
  6. Olaf Beyersdorff. Proof complexity of quantified Boolean logic - a survey. In Marco Benini, Olaf Beyersdorff, Michael Rathjen, and Peter Schuster, editors, Mathematics for Computation (M4C), pages 353-391. World Scientific, 2022. Google Scholar
  7. Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, cost, and capacity: A semantic technique for hard random QBFs. In Proc. Conference on Innovations in Theoretical Computer Science (ITCS'18), pages 9:1-9:18, 2018. Google Scholar
  8. Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan. Building strategies into QBF proofs. J. Autom. Reason., 65(1):125-154, 2021. URL: https://doi.org/10.1007/s10817-020-09560-1.
  9. Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, and Tomás Peitl. Hardness characterisations and size-width lower bounds for QBF resolution. ACM Transactions on Computational Logic, 2022. Google Scholar
  10. Olaf Beyersdorff and Benjamin Böhm. Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021), volume 185 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1-12:20, 2021. Google Scholar
  11. Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, and Jan Pich. Frege systems for quantified Boolean logic. J. ACM, 67(2):9:1-9:36, 2020. Google Scholar
  12. Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. New resolution-based QBF calculi and their proof complexity. ACM Transactions on Computation Theory, 11(4):26:1-26:42, 2019. Google Scholar
  13. Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. Proof complexity of resolution-based QBF calculi. In Proc. Symposium on Theoretical Aspects of Computer Science (STACS'15), pages 76-89. LIPIcs, 2015. Google Scholar
  14. Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, and Martina Seidl. Quantified Boolean formulas. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pages 1177-1221. IOS Press, 2021. Google Scholar
  15. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. Google Scholar
  16. Benjamin Böhm and Olaf Beyersdorff. Lower bounds for QCDCL via formula gauge. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing (SAT), pages 47-63, Cham, 2021. Springer International Publishing. Google Scholar
  17. Benjamin Böhm, Tomás Peitl, and Olaf Beyersdorff. QCDCL with cube learning or pure literal elimination - What is best? In Luc De Raedt, editor, Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI), pages 1781-1787. ijcai.org, 2022. Google Scholar
  18. Benjamin Böhm, Tomás Peitl, and Olaf Beyersdorff. Should decisions in QCDCL follow prefix order? In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 236 of LIPIcs, pages 11:1-11:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  19. 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, Frontiers in Artificial Intelligence and Applications, pages 233-350. IOS Press, 2021. Google Scholar
  20. Mikolás Janota. On Q-Resolution and CDCL QBF solving. In Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 402-418, 2016. Google Scholar
  21. Mikolás Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577:25-42, 2015. Google Scholar
  22. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Inf. Comput., 117(1):12-18, 1995. Google Scholar
  23. Jan Krajíček. Proof complexity, volume 170 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, 2019. Google Scholar
  24. João P. 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, Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. Google Scholar
  25. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Dependency learning for QBF. J. Artif. Intell. Res., 65:180-208, 2019. Google Scholar
  26. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artif. Intell., 175(2):512-525, 2011. URL: https://doi.org/10.1016/j.artint.2010.10.002.
  27. Friedrich Slivovsky. Quantified CDCL with universal resolution. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 236 of LIPIcs, pages 24:1-24:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  28. Allen Van Gelder. Contributions to the theory of practical quantified Boolean formula solving. In Proc. Principles and Practice of Constraint Programming (CP), pages 647-663, 2012. Google Scholar
  29. Moshe Y. Vardi. Boolean satisfiability: theory and engineering. Commun. ACM, 57(3):5, 2014. Google Scholar
  30. Marc Vinyals. Hard examples for common variable decision heuristics. In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI), 2020. Google Scholar
  31. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified Boolean satisfiability solver. In Proc. IEEE/ACM International Conference on Computer-aided Design (ICCAD), pages 442-449, 2002. Google Scholar
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 About DROPS Imprint Privacy Contact