Semi-Algebraic Proof Systems for QBF

TL;DR

This work introduces semi-algebraic proof systems for QBFs, namely $Q\text{-}\mathsf{NS}$, $Q\text{-}\mathsf{SA}$, and $Q\text{-}\mathsf{SOS}$, by augmenting algebraic certificates with universal-variable polynomials and a left-to-right quantifier dependency constraint. It develops a score-game framework to prove completeness and derives both upper and lower bounds, including an exponential $\text{qdeg}_{\exists}$ lower bound for $Q\text{-}\mathsf{SOS}$ on Equality formulas and linear-$\text{qsize}$ refutations for $Q\text{-}\mathsf{Majority}$, yielding separations from $Q\text{-}\mathsf{PC}$ and QU-Res. The paper further adapts propositional techniques via $Q$-pseudo-expectations to obtain lower bounds, and shows strategy extraction via polynomial threshold functions, connecting to $Q$-TC$_0$-Frege. It also establishes a web of simulations among the new systems and classical QBF proofs, clarifying the relative strength and opening several intriguing open questions about incomparability and the true computational model behind strategy extraction. These results lay foundational groundwork for understanding algebraic and semi-algebraic reasoning in the QBF realm, with potential implications for solver design and complexity theory.

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.

Figures (1)

• Figure 1: Simulations and separations between algebraic proof systems in the propositional and the QBF setting. By $P \rightarrow Q$ we indicate that proof system $P$ polynomially simulates $Q$, while $P\ \textcolor{black!50!white}{\dashrightarrow}\ Q$ means that the proof system $P$ does not polynomially simulate $Q$. We omit polynomial (non-)simulations implied by those displayed.

Theorems & Definitions (53)

• Remark 2.2: On variations of $\mathsf{NS}_{}\xspace$, $\mathsf{SA}_{}\xspace$ and $\mathsf{SOS}_{}\xspace$
• Definition 3.1: size, degree, $\mathop{\mathrm{qsize}}\nolimits$ and $\mathop{\mathrm{qdeg_\exists}}\nolimits$
• Theorem 3.2: soundness
• proof
• Remark 3.3: $\mathsf{Q}\text{-}\mathsf{NS}_{}\xspace$ over arbitrary fields
• Remark 3.4: unary vs binary coefficients
• Proposition 3.5
• proof
• Proposition 3.6
• proof