2026-07-22T22:17:56Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23739 2025-08-07T09:32:07Z ddc:004 open_access

Semi-Algebraic Proof Systems for QBF Beyersdorff, Olaf Bonacina, Ilario Kasche, Kaspar Mahajan, Meena Spachmann, Luc Nicolas QBF Proof Complexity Sums-of-Squares Nullstellensatz Sherali-Adams Semi-Algebraic Proof Systems 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Olaf Beyersdorff and Ilario Bonacina and Kaspar Kasche and Meena Mahajan and Luc Nicolas Spachmann 2025 Is Part Of LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2025.5 urn:nbn:de:0030-drops-237394 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.5 eng https://creativecommons.org/licenses/by/4.0/legalcode