Semi-Algebraic Proof Systems for QBF
Olaf Beyersdorff, Ilario Bonacina, Kaspar Kasche, Meena Mahajan, Luc Nicolas Spachmann
我们为量化布尔公式(QBF)引入了新的半代数证明系统,类似于Nullstellensatz,Shereali-Adams和Sum-of-Squares的命题系统。 我们从QBF文献(策略提取)和命题证明复杂性(大小度关系和伪期望)转移到这种设置技术。 我们获得许多强大的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.