Document Open Access Logo

Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution

Authors Olaf Beyersdorff , Benjamin Böhm

PDF
Thumbnail PDF

File

LIPIcs.ITCS.2021.12.pdf
  • Filesize: 0.66 MB
  • 20 pages

Document Identifiers

Author Details

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

Funding

  • Beyersdorff, Olaf: John Templeton Foundation (grant no. 60842), Carl Zeiss Foundation.

Cite As Get BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 185, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ITCS.2021.12

Abstract

QBF solvers implementing the QCDCL paradigm are powerful algorithms that successfully tackle many computationally complex applications. However, our theoretical understanding of the strength and limitations of these QCDCL solvers is very limited.
In this paper we suggest to formally model QCDCL solvers as proof systems. We define different policies that can be used for decision heuristics and unit propagation and give rise to a number of sound and complete QBF proof systems (and hence new QCDCL algorithms). With respect to the standard policies used in practical QCDCL solving, we show that the corresponding QCDCL proof system is incomparable (via exponential separations) to Q-resolution, the classical QBF resolution system used in the literature. This is in stark contrast to the propositional setting where CDCL and resolution are known to be p-equivalent.
This raises the question what formulas are hard for standard QCDCL, since Q-resolution lower bounds do not necessarily apply to QCDCL as we show here. In answer to this question we prove several lower bounds for QCDCL, including exponential lower bounds for a large class of random QBFs. 
We also introduce a strengthening of the decision heuristic used in classical QCDCL, which does not necessarily decide variables in order of the prefix, but still allows to learn asserting clauses. We show that with this decision policy, QCDCL can be exponentially faster on some formulas.
We further exhibit a QCDCL proof system that is p-equivalent to Q-resolution. In comparison to classical QCDCL, this new QCDCL version adapts both decision and unit propagation policies.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • CDCL
  • QBF
  • QCDCL
  • proof complexity
  • resolution
  • Q-resolution

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. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Form. Methods Syst. Des., 41(1):45-65, 2012. Google Scholar
  3. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 154-169, 2014. Google Scholar
  4. 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.
  5. Paul Beame and Toniann Pitassi. Propositional proof complexity: Past, present, and future. In G. Paun, G. Rozenberg, and A. Salomaa, editors, Current Trends in Theoretical Computer Science: Entering the 21st Century, pages 42-70. World Scientific Publishing, 2001. Google Scholar
  6. Olaf Beyersdorff and Joshua Blinkhorn. Lower bound techniques for QBF expansion. Theory Comput. Syst., 64(3):400-421, 2020. Google Scholar
  7. Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate A. Schmidt, and Martin Suda. Reinterpreting dependency schemes: Soundness meets incompleteness in DQBF. J. Autom. Reason., 63(3):597-623, 2019. Google Scholar
  8. Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, cost, and capacity: A semantic technique for hard random QBFs. Logical Methods in Computer Science, 15(1), 2019. Google Scholar
  9. Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan. Building strategies into QBF proofs. In STACS, LIPIcs, pages 14:1-14:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019. Google Scholar
  10. Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan. Hardness characterisations and size-width lower bounds for QBF resolution. In Proc. ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 209-223. ACM, 2020. Google Scholar
  11. Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, and Jan Pich. Frege systems for quantified Boolean logic. J. ACM, 67(2), 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, Meena Mahajan, and Anil Shukla. Feasible interpolation for QBF resolution calculi. Logical Methods in Computer Science, 13, 2017. Google Scholar
  14. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding cutting planes for QBFs. Inf. Comput., 262:141-161, 2018. Google Scholar
  15. Olaf Beyersdorff, Leroy Chew, and Karteek Sreenivasaiah. A game characterisation of tree-like Q-Resolution size. J. Comput. Syst. Sci., 104:82-101, 2019. Google Scholar
  16. Olaf Beyersdorff and Luke Hinde. Characterising tree-like Frege proofs for QBF. Inf. Comput., 268, 2019. Google Scholar
  17. Olaf Beyersdorff, Luke Hinde, and Ján Pich. Reasons for hardness in QBF proof systems. ACM Transactions on Computation Theory, 12(2), 2020. Google Scholar
  18. 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, 2nd edition, Frontiers in Artificial Intelligence and Applications. IOS press, 2021. Google Scholar
  19. Maria Luisa Bonet, Sam Buss, and Jan Johannsen. Improved separations of regular resolution from clause learning proof systems. J. Artif. Intell. Res., 49:669-703, 2014. Google Scholar
  20. Samuel R. Buss. Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic, 163(7):906-917, 2012. Google Scholar
  21. 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), 2008. URL: https://doi.org/10.2168/LMCS-4(4:13)2008.
  22. Marco Cadoli, Andrea Giovanardi, and Marco Schaerf. An algorithm to evaluate quantified Boolean formulae. In Proc. AAAI Conference on Artificial Intelligence (AAAI), pages 262-267, 1998. Google Scholar
  23. Stephen A. Cook and Tsuyoshi Morioka. Quantified propositional calculus and a second-order theory for NC¹. Arch. Math. Log., 44(6):711-749, 2005. Google Scholar
  24. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  25. Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394-397, 1962. URL: https://doi.org/10.1145/368273.368557.
  26. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:210-215, 1960. Google Scholar
  27. Uwe Egly, Florian Lonsing, and Magdalena Widl. Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In Proc. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pages 291-308, 2013. Google Scholar
  28. Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe, and Leander Tentrup. Encodings of bounded synthesis. In Proc. Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference (TACAS), pages 354-370, 2017. Google Scholar
  29. Merrick L. Furst, James B. Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. Mathematical Systems Theory, 17(1):13-27, 1984. Google Scholar
  30. Enrico Giunchiglia, Paolo Marin, and Massimo Narizzano. Reasoning with quantified Boolean formulas. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 761-780. IOS Press, 2009. Google Scholar
  31. Amin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. Google Scholar
  32. Johan Håstad. Computational Limitations of Small Depth Circuits. MIT Press, Cambridge, 1987. Google Scholar
  33. Philipp Hertel, Fahiem Bacchus, Toniann Pitassi, and Allen Van Gelder. Clause learning can effectively p-simulate general propositional resolution. In Proc. AAAI Conference on Artificial Intelligence (AAAI), pages 283-290, 2008. URL: http://www.aaai.org/Library/AAAI/2008/aaai08-045.php.
  34. Marijn J. H. Heule, Martina Seidl, and Armin Biere. Solution validation and extraction for QBF preprocessing. J. Autom. Reason., 58(1):97-125, 2017. Google Scholar
  35. Mikolás Janota. On Q-resolution and CDCL QBF solving. In Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT'16), pages 402-418, 2016. Google Scholar
  36. Mikolás Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577:25-42, 2015. Google Scholar
  37. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Inf. Comput., 117(1):12-18, 1995. Google Scholar
  38. Jan Krajíček. Proof complexity, volume 170 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, 2019. Google Scholar
  39. Florian Lonsing. Dependency Schemes and Search-Based QBF Solving: Theory and Practice. PhD thesis, Johannes Kepler University Linz, 2012. Google Scholar
  40. Florian Lonsing and Uwe Egly. DepQBF 6.0: A search-based QBF solver beyond traditional QCDCL. In Proc. International Conference on Automated Deduction (CADE), pages 371-384, 2017. Google Scholar
  41. Florian Lonsing, Uwe Egly, and Allen Van Gelder. Efficient clause learning for quantified Boolean formulas via QBF pseudo unit propagation. In Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 100-115, 2013. Google Scholar
  42. João P. Marques Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Handbook of Satisfiability. IOS Press, 2009. Google Scholar
  43. João P. Marques Silva and Karem A. Sakallah. GRASP - a new search algorithm for satisfiability. In ICCAD, pages 220-227, 1996. URL: https://doi.org/10.1145/244522.244560.
  44. Nathan Mull, Shuo Pang, and Alexander A. Razborov. On CDCL-based proof systems with the ordered decision strategy. In Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT'20), pages 149-165. Springer, 2020. Google Scholar
  45. Jakob Nordström. Short Proofs May Be Spacious : Understanding Space in Resolution. PhD thesis, Royal Institute of Technology, Stockholm, Sweden, 2008. Google Scholar
  46. Jakob Nordström. On the interplay between proof complexity and SAT solving. SIGLOG News, 2(3):19-44, 2015. Google Scholar
  47. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Dependency learning for QBF. J. Artif. Intell. Res., 65:180-208, 2019. Google Scholar
  48. 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.
  49. Luca Pulina and Martina Seidl. The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17). Artif. Intell., 274:224-248, 2019. Google Scholar
  50. Nathan Segerlind. The complexity of propositional proofs. Bulletin of Symbolic Logic, 13(4):417-481, 2007. Google Scholar
  51. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified Boolean formulas. In Proc. IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pages 78-84, 2019. Google Scholar
  52. Friedrich Slivovsky and Stefan Szeider. Soundness of Q-resolution with dependency schemes. Theoretical Computer Science, 612:83-101, 2016. Google Scholar
  53. Moshe Y. Vardi. Boolean satisfiability: theory and engineering. Commun. ACM, 57(3):5, 2014. Google Scholar
  54. Marc Vinyals. Hard examples for common variable decision heuristics. In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI), 2020. Google Scholar
  55. Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, and Sharad Malik. Efficient conflict driven learning in Boolean satisfiability solver. In Proc. IEEE/ACM International Conference on Computer-Aided Design (ICCAD), pages 279-285, 2001. Google Scholar
  56. 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