Document Open Access Logo

Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree

Authors Olaf Beyersdorff , Tim Hoffmann , Kaspar Kasche , Luc Nicolas Spachmann

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2024.27.pdf
  • Filesize: 0.74 MB
  • 15 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • proof complexity
  • QBF
  • polynomial calculus
  • circuits
  • lower bounds

Metrics

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

Abstract

We initiate an in-depth proof-complexity analysis of polynomial calculus (𝒬-PC) for Quantified Boolean Formulas (QBF). In the course of this we establish a tight proof-size characterisation of 𝒬-PC in terms of a suitable circuit model (polynomial decision lists). Using this correspondence we show a size-degree relation for 𝒬-PC, similar in spirit, yet different from the classic size-degree formula for propositional PC by Impagliazzo, Pudlák and Sgall (1999).
We use the circuit characterisation together with the size-degree relation to obtain various new lower bounds on proof size in 𝒬-PC. This leads to incomparability results for 𝒬-PC systems over different fields.

Cite As Get BibTex

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 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.MFCS.2024.27

Author Details

Olaf Beyersdorff
  • Friedrich Schiller University Jena, Germany
Tim Hoffmann
  • Friedrich Schiller University Jena, Germany
Kaspar Kasche
  • Friedrich Schiller University Jena, Germany
Luc Nicolas Spachmann
  • Friedrich Schiller University Jena, Germany

Funding

  • Beyersdorff, Olaf: Carl-Zeiss Foundation and DFG grant BE 4209/3-1
  • Hoffmann, Tim: Carl-Zeiss Foundation
  • Kasche, Kaspar: Carl-Zeiss Foundation

References

  1. Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach. Cambridge University Press, 2009. URL: http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521424264.
  2. 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.
  3. 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.
  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. URL: https://doi.org/10.1007/978-3-319-09284-3_12.
  5. Paul Beame, Henry A. Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res., 22:319-351, 2004. URL: https://doi.org/10.1613/jair.1410.
  6. 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
  7. 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.
  8. Olaf Beyersdorff. On the correspondence between arithmetic theories and propositional proof systems - a survey. Mathematical Logic Quarterly, 55(2):116-137, 2009. URL: https://doi.org/10.1002/malq.200710069.
  9. 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
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Are short proofs narrow? QBF resolution is not so simple. ACM Trans. Comput. Log., 19(1):1:1-1:26, 2018. URL: https://doi.org/10.1145/3157053.
  16. Olaf Beyersdorff and Luke Hinde. Characterising tree-like Frege proofs for QBF. Inf. Comput., 268, 2019. URL: https://doi.org/10.1016/j.ic.2019.05.002.
  17. 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.
  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, Frontiers in Artificial Intelligence and Applications, pages 1177-1221. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201015.
  19. Olaf Beyersdorff and Oliver Kutz. Proof complexity of non-classical logics. In N. Bezhanishvili and V. Goranko, editors, Lectures on Logic and Computation - ESSLLI 2010 /ESSLLI 2011, Selected Lecture Notes, pages 1-54. Springer-Verlag, Berlin Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-31485-8_1.
  20. 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.
  21. 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. URL: https://doi.org/10.24963/ijcai.2022/248.
  22. Nader H. Bshouty. A subexponential exact learning algorithm for DNF using equivalence queries. Inf. Process. Lett., 59(1):37-39, 1996. URL: https://doi.org/10.1016/0020-0190(96)00077-4.
  23. 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.
  24. 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.
  25. Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proc. 28th ACM Symposium on Theory of Computing, pages 174-183, 1996. URL: https://doi.org/10.1145/237814.237860.
  26. Jonas Conneryd, Susanna F. de Rezende, Jakob Nordström, Shuo Pang, and Kilian Risse. Graph colouring is hard on average for polynomial calculus and Nullstellensatz. In 64th IEEE Annual Symposium on Foundations of Computer Science (FOCS), pages 1-11. IEEE, 2023. URL: https://doi.org/10.1109/FOCS57990.2023.00007.
  27. Stephen A. Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. Cambridge University Press, 2010. Google Scholar
  28. 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.
  29. Susanna F. de Rezende, Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, and Dmitry Sokolov. Automating algebraic proof systems is NP-hard. In Samir Khuller and Virginia Vassilevska Williams, editors, 53rd Annual ACM SIGACT Symposium on Theory of Computing (STOC), pages 209-222. ACM, 2021. URL: https://doi.org/10.1145/3406325.3451080.
  30. 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.
  31. Michael A. Forbes, Amir Shpilka, Iddo Tzameret, and Avi Wigderson. Proof complexity lower bounds from algebraic circuit complexity. Theory Comput., 17:1-88, 2021. URL: https://theoryofcomputing.org/articles/v017a010/.
  32. Nicola Galesi, Joshua A. Grochow, Toniann Pitassi, and Adrian She. On the algebraic proof complexity of tensor isomorphism. In Amnon Ta-Shma, editor, 38th Computational Complexity Conference (CCC), volume 264 of LIPIcs, pages 4:1-4:40. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CCC.2023.4.
  33. Alexandra Goultiaeva, Allen Van Gelder, and Fahiem Bacchus. A uniform approach for generating proofs and strategies for both true and false QBF formulas. In IJCAI, pages 546-553, 2011. URL: https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-099.
  34. Nashlen Govindasamy, Tuomas Hakoniemi, and Iddo Tzameret. Simple hard instances for low-depth algebraic proofs. In 63rd IEEE Annual Symposium on Foundations of Computer Science (FOCS), pages 188-199. IEEE, 2022. URL: https://doi.org/10.1109/FOCS54457.2022.00025.
  35. Joshua A. Grochow and Toniann Pitassi. Circuit complexity, proof complexity, and polynomial identity testing: The ideal proof system. J. ACM, 65(6):37:1-37:59, 2018. URL: https://doi.org/10.1145/3230742.
  36. Pavel Hrubeš. On lengths of proofs in non-classical logics. Ann. Pure Appl. Logic, 157(2-3):194-205, 2009. URL: https://doi.org/10.1016/j.apal.2008.09.013.
  37. Russell Impagliazzo, Pavel Pudlák, and Jirí Sgall. Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Comput. Complex., 8(2):127-144, 1999. URL: https://doi.org/10.1007/s000370050024.
  38. 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.
  39. Jan Krajíček. Bounded Arithmetic, Propositional Logic, and Complexity Theory, volume 60 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge, 1995. Google Scholar
  40. Jan Krajíček. Proof complexity, volume 170 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, 2019. Google Scholar
  41. Serge Lang. Algebra (3. ed.). Addison-Wesley, 1993. Google Scholar
  42. 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.
  43. Toniann Pitassi and Iddo Tzameret. Algebraic proof complexity: progress, frontiers and challenges. SIGLOG News, 3(3):21-43, 2016. URL: https://doi.org/10.1145/2984450.2984455.
  44. 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.
  45. Ronald L. Rivest. Learning decision lists. Machine Learning, 2(3):229-246, 1987. URL: https://doi.org/10.1007/BF00058680.
  46. Sarah Sigley and Olaf Beyersdorff. Proof complexity of modal resolution. J. Autom. Reason., 66(1):1-41, 2022. URL: https://doi.org/10.1007/s10817-021-09609-9.
  47. R. Smolensky. Algebraic methods in the theory of lower bounds for boolean circuit complexity. In Proc. ACM Symposium on Theory of Computing (STOC), pages 77-82. ACM Press, 1987. URL: https://doi.org/10.1145/28395.28404.
  48. Heribert Vollmer. Introduction to Circuit Complexity - A Uniform Approach. Texts in Theoretical Computer Science. Springer Verlag, Berlin Heidelberg, 1999. URL: https://doi.org/10.1007/978-3-662-03927-4.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact