Document Open Access Logo

Towards Understanding the Complexity of CAQE: A Proof-Theoretic Analysis of Its Core Procedure

Authors Benjamin Böhm , Olaf Beyersdorff

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.7.pdf
  • Filesize: 0.96 MB
  • 20 pages

Document Identifiers

Subject Classification

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

Metrics

Abstract

CAQE (Clausal Abstraction for Quantifier Elimination) is currently the most successful algorithmic paradigm for solving Quantified Boolean Formulas (QBF) practice-wise, clearly dominating recent QBF competitions. While apparently being a very strong solver, not much is known about CAQE theory-wise. We propose a framework for formalising runs in the basic CAQE algorithm (where failed assumptions are not considered) as proofs in a proof system CAQE^CORE, which we use to analyse the algorithm proof-theoretically and provide methods for future work to separate it from optimized versions of CAQE that are used in practice.
We show that one can perform strategy extraction on the CAQE^CORE proof system in such a way that strategy size serves as a lower bound for basic CAQE runs. Furthermore, we introduce a measure, which we call CAQE width, which not only acts as a lower bound on CAQE^CORE proofs, but - with the quantifier depth as exponent - as an upper bound as well. Using this analysis, we prove that on QBFs of bounded quantifier complexity, both QCDCL (Quantified Conflict Driven Clause Learning, formalised as a proof system) and Q-resolution p-simulate CAQE^CORE and are indeed strictly stronger.

Cite As Get BibTex

Benjamin Böhm and Olaf Beyersdorff. Towards Understanding the Complexity of CAQE: A Proof-Theoretic Analysis of Its Core Procedure. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.7

Author Details

Benjamin Böhm
  • Friedrich Schiller University Jena, Germany
Olaf Beyersdorff
  • Friedrich Schiller University Jena, Germany

Funding

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

Acknowledgements

We thank Leroy Chew for asking a question at SAT'25 on the proof-theoretic strength of CAQE, which led to this work.

References

  1. 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. URL: https://doi.org/10.1007/978-3-319-09284-3_12.
  2. 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, Singapore, 2022. Google Scholar
  3. 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. URL: https://doi.org/10.23638/LMCS-15(1:13)2019.
  4. Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, and Tomás Peitl. Hardness characterisations and size-width lower bounds for QBF resolution. ACM Trans. Comput. Log., 24(2):10:1-10:30, 2023. URL: https://doi.org/10.1145/3565286.
  5. Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, and Gaurav Sood. Hard QBFs for merge resolution. ACM Trans. Comput. Theory, 16(2):6:1-6:24, 2024. URL: https://doi.org/10.1145/3638263.
  6. Olaf Beyersdorff and Benjamin Böhm. Understanding the relative strength of QBF CDCL solvers and QBF resolution. Log. Methods Comput. Sci., 19(2), 2023. URL: https://doi.org/10.46298/LMCS-19(2:2)2023.
  7. Olaf Beyersdorff, Benjamin Böhm, and Meena Mahajan. Runtime vs. extracted proof size: An exponential gap for CDCL on QBFs. J. Autom. Reason., 69(4):30, 2025. URL: https://doi.org/10.1007/S10817-025-09745-6.
  8. Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, and Jan Pich. Frege systems for quantified Boolean logic. J. ACM, 67(2):9:1-9:36, 2020. URL: https://doi.org/10.1145/3381881.
  9. Olaf Beyersdorff, Ilario Bonacina, Kaspar Kasche, Meena Mahajan, and Luc Nicolas Spachmann. Semi-algebraic proof systems for QBF. In Jeremias Berg and Jakob Nordström, editors, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 341 of LIPIcs, pages 5:1-5:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.SAT.2025.5.
  10. 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. URL: https://doi.org/10.1145/3352155.
  11. Olaf Beyersdorff, Luke Hinde, and Ján Pich. Reasons for hardness in QBF proof systems. ACM Transactions on Computation Theory, 12(2):10:1-10:27, 2020. URL: https://doi.org/10.1145/3378665.
  12. Olaf Beyersdorff, Tim Hoffmann, and Luc Nicolas Spachmann. Proof complexity of propositional model counting. J. Satisf. Boolean Model. Comput., 15(1):27-59, 2024. URL: https://doi.org/10.3233/SAT-231507.
  13. 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. URL: https://doi.org/10.3233/FAIA201015.
  14. Benjamin Böhm and Olaf Beyersdorff. Lower bounds for QCDCL via formula gauge. J. Autom. Reason., 67(4):35, 2023. URL: https://doi.org/10.1007/S10817-023-09683-1.
  15. Benjamin Böhm and Olaf Beyersdorff. QCDCL vs QBF resolution: Further insights. J. Artif. Intell. Res., 81:741-769, 2024. URL: https://doi.org/10.1613/JAIR.1.15522.
  16. Benjamin Böhm, Tomás Peitl, and Olaf Beyersdorff. QCDCL with cube learning or pure literal elimination - what is best? Artif. Intell., 336:104194, 2024. URL: https://doi.org/10.1016/J.ARTINT.2024.104194.
  17. Benjamin Böhm, Tomás Peitl, and Olaf Beyersdorff. Should decisions in QCDCL follow prefix order? J. Autom. Reason., 68(1):5, 2024. URL: https://doi.org/10.1007/S10817-024-09694-6.
  18. 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. URL: https://doi.org/10.3233/FAIA200990.
  19. Leroy Chew and Marijn J. H. Heule. Relating existing powerful proof systems for QBF. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 236 of LIPIcs, pages 10:1-10:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.10.
  20. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  21. 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. URL: https://doi.org/10.1007/978-3-642-45221-5_21.
  22. Marijn J. H. Heule, Martina Seidl, and Armin Biere. Solution validation and extraction for QBF preprocessing. J. Autom. Reason., 58(1):97-125, 2017. URL: https://doi.org/10.1007/S10817-016-9390-4.
  23. Mikolás Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577:25-42, 2015. URL: https://doi.org/10.1016/J.TCS.2015.01.048.
  24. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Inf. Comput., 117(1):12-18, 1995. URL: https://doi.org/10.1006/INCO.1995.1025.
  25. 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. URL: https://doi.org/10.1007/978-3-319-63046-5_23.
  26. 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. URL: https://doi.org/10.3233/FAIA200987.
  27. 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.
  28. 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.
  29. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Qute in the QBF evaluation 2018. J. Satisf. Boolean Model. Comput., 11(1):261-272, 2019. URL: https://doi.org/10.3233/SAT190124.
  30. Luca Pulina and Martina Seidl. The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17). Artif. Intell., 274:224-248, 2019. URL: https://doi.org/10.1016/J.ARTINT.2019.04.002.
  31. QBF solver evaluation portal. URL: https://www.qbflib.org/index_eval.php.
  32. Markus N. Rabe and Leander Tentrup. CAQE: A certifying QBF solver. In Roope Kaivola and Thomas Wahl, editors, Formal Methods in Computer-Aided Design (FMCAD), pages 136-143. IEEE, 2015. URL: https://doi.org/10.1109/FMCAD.2015.7542263.
  33. Ronald L. Rivest. Learning decision lists. Machine Learning, 2(3):229-246, 1987. URL: https://doi.org/10.1007/BF00058680.
  34. 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. URL: https://doi.org/10.1109/ICTAI.2019.00020.
  35. Leander Tentrup. On expansion and resolution in CEGAR based QBF solving. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pages 475-494. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_25.
  36. Leander Tentrup. CAQE and quabs: Abstraction based QBF solvers. J. Satisf. Boolean Model. Comput., 11(1):155-210, 2019. URL: https://doi.org/10.3233/SAT190121.
  37. 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. URL: https://doi.org/10.1007/978-3-642-33558-7_47.
  38. 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. URL: https://doi.org/10.1145/774572.774637.
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