Semi-Algebraic Proof Systems for QBF

2025/11/11 by Olaf Beyersdorff, Beyersdorff, Olaf, Ilario Bonacina +7
Computer Science · #03D15 #03F20 #Complexity and Algorithms in Graphs #Computational Complexity (cs.CC) #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.2511.08050

openalex publication_date 2025/11/11 · openalex created_date 2025/11/13 · openalex updated_date 2026/08/01

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.

Citations

• Proof complexity and the binary encoding of combinatorial principles
• Sherali-Adams and the binary encoding of combinatorial principles
• Size-Degree Trade-Offs for Sums-of-Squares and Positivstellensatz Proofs
• Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
• Narrow Proofs May Be Maximally Long
• Approximability and proof complexity
• A Hierarchy of Relaxations between the Continuous and Convex Hull Representations for Zero-One Programming Problems

Related

• Proof Complexity of Symbolic QBF Reasoning
• On Stronger Calculi for QBFs
• On QBF Proofs and Preprocessing
• Short Proofs for Some Symmetric Quantified Boolean Formulas
• On Expansion and Resolution in CEGAR Based QBF Solving