Document Open Access Logo

Dependency Schemes in CDCL-Based QBF Solving: A Proof-Theoretic Study

Authors Abhimanyu Choudhury , Meena Mahajan

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2023.38.pdf
  • Filesize: 0.78 MB
  • 18 pages

Document Identifiers

Author Details

Abhimanyu Choudhury
  • The Institute of Mathematical Sciences, Chennai, India
  • Homi Bhabha National Institute, Training School Complex, Anushaktinagar, Mumbai, India
Meena Mahajan
  • The Institute of Mathematical Sciences, Chennai, India
  • Homi Bhabha National Institute, Training School Complex, Anushaktinagar, Mumbai, India

Acknowledgements

Part of this work was done when the second author was at the Simons Institute for the Theory of Computing at Berkeley during March-May 2023, participating in the Extended Reunion of the program Satisfiability: Theory, Practice, and Beyond.

Cite AsGet BibTex

Abhimanyu Choudhury and Meena Mahajan. Dependency Schemes in CDCL-Based QBF Solving: A Proof-Theoretic Study. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSTTCS.2023.38

Abstract

In Quantified Boolean Formulas QBFs, dependency schemes help to detect spurious or superfluous dependencies that are implied by the variable ordering in the quantifier prefix but are not essential for constructing countermodels. This detection can provably shorten refutations in specific proof systems, and is expected to speed up runs of QBF solvers. The proof system QCDCL recently defined by Beyersdorff and Böhm (LMCS 2023) abstracts the reasoning employed by QBF solvers based on conflict-driven clause-learning (CDCL) techniques. We show how to incorporate the use of dependency schemes into this proof system, either in a preprocessing phase, or in the propagations and clause learning, or both. We then show that when the reflexive resolution path dependency scheme 𝙳^rrs is used, a mixed picture emerges: the proof systems that add 𝙳^rrs to QCDCL in these three ways are not only incomparable with each other, but are also incomparable with the basic QCDCL proof system that does not use 𝙳^rrs at all, as well as with several other resolution-based QBF proof systems. A notable fact is that all our separations are achieved through QBFs with bounded quantifier alternation.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • QBF
  • CDCL
  • Resolution
  • Dependency schemes

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. URL: https://doi.org/10.1613/jair.3152.
  2. Salman Azhar, Gary Peterson, and John Reif. Lower bounds for multiplayer non-cooperative games of incomplete information. Journal of Computers and Mathematics with Applications, 41:957-992, 2001. Google Scholar
  3. Olaf Beyersdorff and Joshua Blinkhorn. Dynamic QBF dependencies in reduction and expansion. ACM Trans. Comput. Log., 21(2):8:1-8:27, 2020. URL: https://doi.org/10.1145/3355995.
  4. Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, cost, and capacity: A semantic technique for hard random QBFs. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:13)2019.
  5. Olaf Beyersdorff, Joshua Blinkhorn, and Tomás Peitl. Strong (D)QBF dependency schemes via tautology-free resolution paths. 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 394-411. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_28.
  6. Olaf Beyersdorff, Joshua Blinkhorn, and Tomás Peitl. Strong (D)QBF dependency schemes via implication-free resolution paths. Electron. Colloquium Comput. Complex., TR21-135, 2021. URL: https://arxiv.org/abs/TR21-135.
  7. Olaf Beyersdorff and Benjamin Böhm. Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. Logical Methods in Computer Science, Volume 19, Issue 2, April 2023. (Preliminary version in ITCS'21). URL: https://doi.org/10.46298/lmcs-19(2:2)2023.
  8. Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theory, 11(4):26:1-26:42, 2019. URL: https://doi.org/10.1145/3352155.
  9. 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 - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 1177-1221. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201015.
  10. Joshua Blinkhorn and Olaf Beyersdorff. Shortening QBF proofs with dependency schemes. In Theory and Applications of Satisfiability Testing - SAT, volume 10491 of LNCS, pages 263-280. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_17.
  11. Benjamin Böhm, Tomás Peitl, and Olaf Beyersdorff. Should decisions in QCDCL follow prefix order? In 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, pages 11:1-11:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.11.
  12. Benjamin Böhm and Olaf Beyersdorff. QCDCL vs QBF resolution: Further insights. In 26th Theory and Applications of Satisfiability Testing - SAT, 2023. full version in ECCC, TR23-051. Google Scholar
  13. Benjamin Böhm, Tomáš Peitl, and Olaf Beyersdorff. QCDCL with cube learning or pure literal elimination - What is best? In Lud De Raedt, editor, Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22, pages 1781-1787. International Joint Conferences on Artificial Intelligence Organization, July 2022. Main Track. URL: https://doi.org/10.24963/ijcai.2022/248.
  14. Abhimanyu Choudhury and Meena Mahajan. Dependency schemes in CDCL-based QBF solving: a proof-theoretic study. Electron. Colloquium Comput. Complex., TR23-061, 2023. URL: https://arxiv.org/abs/TR23-061.
  15. Florian Lonsing. Dependency schemes and search-based QBF solving: theory and practice. PhD thesis, Johannes Kepler University, Linz, Austria, 2012. Google Scholar
  16. Florian Lonsing and Armin Biere. Depqbf: A dependency-aware QBF solver. J. Satisf. Boolean Model. Comput., 7(2-3):71-76, 2010. URL: https://doi.org/10.3233/sat190077.
  17. Florian Lonsing and Armin Biere. Integrating dependency schemes in search-based QBF solvers. In Ofer Strichman and Stefan Szeider, editors, Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6175 of Lecture Notes in Computer Science, pages 158-171. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14186-7_14.
  18. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Dependency learning for QBF. J. Artif. Intell. Res., 65:180-208, 2019. URL: https://doi.org/10.1613/jair.1.11529.
  19. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Long-distance Q-resolution with dependency schemes. J. Autom. Reasoning, 63(1):127-155, 2019. URL: https://doi.org/10.1007/s10817-018-9467-3.
  20. 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.
  21. Marko Samer and Stefan Szeider. Backdoor sets of quantified boolean formulas. J. Autom. Reason., 42(1):77-97, 2009. URL: https://doi.org/10.1007/s10817-008-9114-5.
  22. Christoph Scholl and Ralf Wimmer. Dependency quantified Boolean formulas: An overview of solution methods and applications - extended abstract. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, International Conference on Theory and Practice of Satisfiability Testing SAT, volume 10929 of LNCS, pages 3-16. Springer, 2018. Google Scholar
  23. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified boolean formulas. In 31st IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2019, Portland, OR, USA, November 4-6, 2019, pages 78-84. IEEE, 2019. URL: https://doi.org/10.1109/ICTAI.2019.00020.
  24. Friedrich Slivovsky and Stefan Szeider. Soundness of Q-resolution with dependency schemes. Theor. Comput. Sci., 612:83-101, 2016. URL: https://doi.org/10.1016/j.tcs.2015.10.020.
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