Semi-Algebraic Proof Systems for QBF

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.

Authors

• Olaf Beyersdorff
• Ilario Bonacina
• Kaspar Kasche
• Meena Mahajan
• Luc Nicolas Spachmann

Keywords

• QBF
• Proof Complexity
• Sums-of-Squares
• Nullstellensatz
• Sherali-Adams
• Semi-Algebraic Proof Systems