Document Open Access Logo

Semi-Algebraic Proof Systems for QBF

Authors Olaf Beyersdorff , Ilario Bonacina , Kaspar Kasche , Meena Mahajan , Luc Nicolas Spachmann

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2025.5.pdf
  • Filesize: 0.95 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Complexity theory and logic
Keywords
  • QBF
  • Proof Complexity
  • Sums-of-Squares
  • Nullstellensatz
  • Sherali-Adams
  • Semi-Algebraic Proof Systems

Metrics

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

Abstract

We introduce new semi-algebraic proof systems for Quantified Boolean Formulas (QBF) analogous to the propositional systems Nullstellensatz, Sherali-Adams and Sum-of-Squares. We transfer to this setting techniques both from the QBF literature (strategy extraction) and from propositional proof complexity (size-degree relations and pseudo-expectation). We obtain a number of strong QBF lower bounds and separations between these systems, even when disregarding propositional hardness.

Cite As Get BibTex

Olaf Beyersdorff, Ilario Bonacina, Kaspar Kasche, Meena Mahajan, and Luc Nicolas Spachmann. Semi-Algebraic Proof Systems for QBF. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.5

Author Details

Olaf Beyersdorff
  • Friedrich Schiller University Jena, Germany
Ilario Bonacina
  • UPC Universitat Politècnica de Catalunya, Barcelona, Spain
Kaspar Kasche
  • Friedrich Schiller University Jena, Germany
Meena Mahajan
  • The Institute of Mathematical Sciences (A CI of Homi Bhabha National Institute), Chennai, India
Luc Nicolas Spachmann
  • Friedrich Schiller University Jena, Germany

Funding

  • Beyersdorff, Olaf: Carl-Zeiss Foundation and DFG grant BE 4209/3-1.
  • Bonacina, Ilario: This author was funded by the AEI with the grant number PID2022-138506NB-C22.
  • Kasche, Kaspar: Carl-Zeiss Foundation.
  • Mahajan, Meena: Supported in part by the J. C. Bose Fellowship of SERB, ANRF.

Acknowledgements

The authors would like to thank the Oberwolfach Research Institute for Mathematics: the idea for this work started during the Oberwolfach workshop 2413 "Proof Complexity and Beyond", and the Schloss Dagstuhl – Leibniz Center for Informatics: part of this work has been done during the Dagstuhl Seminar 24421 "SAT and Interactions".

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. Albert Atserias and Tuomas Hakoniemi. Size-Degree Trade-Offs for Sums-of-Squares and Positivstellensatz Proofs. In 34th Computational Complexity Conference (CCC 2019), volume 137, pages 24:1-24:20, 2019. URL: https://doi.org/10.4230/LIPICS.CCC.2019.24.
  3. Albert Atserias, Massimo Lauria, and Jakob Nordström. Narrow proofs may be maximally long. In 29th Conference on Computational Complexity (CCC 2014), pages 286-297, 2014. URL: https://doi.org/10.1109/CCC.2014.36.
  4. Albert Atserias, Massimo Lauria, and Jakob Nordström. Narrow proofs may be maximally long. ACM Trans. Comput. Logic, 17(3):19:1-19:30, 2016. A preliminary version of this work appeared as [Albert Atserias et al., 2014]. URL: https://doi.org/10.1145/2898435.
  5. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Form. Methods Syst. Des., 41(1):45-65, 2012. URL: https://doi.org/10.1007/s10703-012-0152-6.
  6. 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.
  7. Boaz Barak, Fernando G.S.L. Brandao, Aram W. Harrow, Jonathan Kelner, David Steurer, and Yuan Zhou. Hypercontractivity, sum-of-squares proofs, and their applications. In 44th Annual ACM Symposium on Theory of Computing (STOC 2012), pages 307-326, 2012. URL: https://doi.org/10.1145/2213977.2214006.
  8. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - Resolution made simple. J. ACM, 48(2):149-169, 2001. URL: https://doi.org/10.1145/375827.375835.
  9. Christoph Berkholz. The Relation between Polynomial Calculus, Sherali-Adams, and Sum-of-Squares Proofs. In 35th Symposium on Theoretical Aspects of Computer Science (STACS), volume 96, pages 11:1-11:14, 2018. URL: https://doi.org/10.4230/LIPIcs.STACS.2018.11.
  10. 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
  11. 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. URL: https://doi.org/10.4230/LIPICS.ITCS.2018.9.
  12. 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. A preliminary version of this work appeared as [Beyersdorff et al., 2018]. URL: https://doi.org/10.23638/LMCS-15(1:13)2019.
  13. 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.
  14. 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.
  15. Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew. Lower bounds: From circuits to QBF proof systems. In Proc. ACM Conference on Innovations in Theoretical Computer Science (ITCS'16), pages 249-260, 2016. URL: https://doi.org/10.1145/2840728.2840740.
  16. Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, and Jan Pich. Frege systems for quantified Boolean logic. J. ACM, 67(2):9:1-9:36, 2020. Preliminary versions of this work appeared as [Beyersdorff et al., 2016] and [Olaf Beyersdorff and Ján Pich, 2016]. URL: https://doi.org/10.1145/3381881.
  17. 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.
  18. 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. URL: https://doi.org/10.4230/LIPIcs.STACS.2015.76.
  19. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding cutting planes for QBFs. Inf. Comput., 262:141-161, 2018. URL: https://doi.org/10.1016/j.ic.2018.08.002.
  20. 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.
  21. Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche, and Luc Nicolas Spachmann. Polynomial calculus for quantified boolean logic: Lower bounds through circuits and degree. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 306, pages 27:1-27:15, 2024. URL: https://doi.org/10.4230/LIPICS.MFCS.2024.27.
  22. 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. URL: https://doi.org/10.3233/FAIA201015.
  23. Olaf Beyersdorff and Ján Pich. Understanding Gentzen and Frege systems for QBF. In Proc. ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016. URL: https://doi.org/10.1145/2933575.2933597.
  24. A. Blake. Canonical expressions in boolean algebra. PhD thesis, University of Chicago, 1937. Google Scholar
  25. Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy. Weighted, circular and semi-algebraic proofs. J. Artif. Intell. Res., 79:447-482, 2024. A preliminary version of this work appeared as [Maria Luisa Bonet and Jordi Levy, 2020]. URL: https://doi.org/10.1613/JAIR.1.15075.
  26. Maria Luisa Bonet and Jordi Levy. Equivalence between systems stronger than resolution. In 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT 2020), volume 12178, pages 166-181, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_13.
  27. Sam Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. Linear gaps between degrees for the polynomial calculus modulo distinct primes. Journal of Computer and System Sciences, 62(2):267-289, 2001. URL: https://doi.org/10.1006/jcss.2000.1726.
  28. 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.
  29. Sravanthi Chede, Leroy Chew, Balesh Kumar, and Anil Shukla. Understanding Nullstellensatz for QBFs. Electron. Colloquium Comput. Complex., TR23-129, 2023. URL: https:TR//eccc.weizmann.ac.il/report/2023/129/.
  30. Hubie Chen. Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. ACM Transactions on Computation Theory, 9(3):15:1-15:20, 2017. URL: https://doi.org/10.1145/3087534.
  31. Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In 28th Annual ACM Symposium on the Theory of Computing (STOC), pages 174-183, 1996. URL: https://doi.org/10.1145/237814.237860.
  32. 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.
  33. William Cook, Collette R. Coullard, and György Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  34. Stefan S. Dantchev, Nicola Galesi, Abdul Ghani, and Barnaby Martin. Proof complexity and the binary encoding of combinatorial principles. SIAM J. Comput., 53(3):764-802, 2024. A preliminary version appeared as [Stefan S. Dantchev et al., 2020]. URL: https://doi.org/10.1137/20M134784X.
  35. Stefan S. Dantchev, Abdul Ghani, and Barnaby Martin. Sherali-adams and the binary encoding of combinatorial principles. In 14th Latin American Symposium on Theoretical Informatics (LATIN 2020), volume 12118, pages 336-347, 2020. URL: https://doi.org/10.1007/978-3-030-61792-9_27.
  36. Stefan S. Dantchev and Barnaby Martin. Rank complexity gap for lovász-schrijver and sherali-adams proof systems. Comput. Complex., 22(1):191-213, 2013. URL: https://doi.org/10.1007/S00037-012-0049-1.
  37. Stefan S. Dantchev, Barnaby Martin, and Mark Nicholas Charles Rhodes. Tight rank lower bounds for the Sherali-Adams proof system. Theor. Comput. Sci., 410(21-23):2054-2063, 2009. URL: https://doi.org/10.1016/J.TCS.2009.01.002.
  38. Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov. The power of negative reasoning. In 36th Computational Complexity Conference (CCC), volume 200, pages 40:1-40:24, 2021. URL: https://doi.org/10.4230/LIPICS.CCC.2021.40.
  39. 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.
  40. Noah Fleming, Pravesh Kothari, and Toniann Pitassi. Semialgebraic proofs and efficient algorithm design. Found. Trends Theor. Comput. Sci., 14(1-2):1-221, 2019. URL: https://doi.org/10.1561/0400000086.
  41. Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Separations in proof complexity and TFNP. J. ACM, 71(4):26:1-26:45, 2024. URL: https://doi.org/10.1145/3663758.
  42. Tuomas Hakoniemi. Feasible interpolation for polynomial calculus and sums-of-squares. In 47th International Colloquium on Automata, Languages, and Programming (ICALP), volume 168, pages 63:1-63:14, 2020. URL: https://doi.org/10.4230/LIPICS.ICALP.2020.63.
  43. 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.
  44. 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.
  45. Jean B. Lasserre. Global optimization with polynomials and the problem of moments. SIAM J. Optim., 11(3):796-817, 2001. URL: https://doi.org/10.1137/S1052623400366802.
  46. Marvin Minsky and Seymour Papert. Perceptrons - An introduction to computational geometry. MIT Press, 1987. URL: https://doi.org/10.7551/mitpress/11301.001.0001.
  47. Ryan O'Donnell and Yuan Zhou. Approximability and proof complexity. In Proceedings of the Twenty-Fourth Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 1537-1556. SIAM, 2013. URL: https://doi.org/10.1137/1.9781611973105.111.
  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. John Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12:23-41, 1965. URL: https://doi.org/10.1145/321250.321253.
  50. Hanif D. Sherali and Warren P. Adams. A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems. SIAM J. Discret. Math., 3(3):411-430, 1990. URL: https://doi.org/10.1137/0403036.
  51. Dmitry Sokolov. (semi)algebraic proofs over ±1 variables. In Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing (STOC), pages 78-90, 2020. URL: https://doi.org/10.1145/3357713.3384288.
  52. 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.
  53. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact