Towards Uniform Certification in QBF

TL;DR

The paper addresses the challenge of universal QBF proof checking by showing that extended Frege with universal reduction, $\mathsf{eFrege}$+$\boldsymbol{\forall}$\mathsf{red}$, p-simulates a broad family of QBF proof systems, including M-Res, IR-calc, IRM-calc, and LQU$^+$-Res. It achieves this through strategy-extraction techniques that translate winning strategies into local, propositional strategies encoded via extension variables and policy constructs, enabling largely propositional interpretations of these systems. The results strengthen the case for uniform certification in QBF solving and imply potential universal checking formats such as QRAT, while providing explicit constructions for how to convert and simulate each calculus within the $\mathsf{eFrege}$+$\boldsymbol{\forall}$\mathsf{red}$ framework. The paper also highlights local strategy extraction methods and four-valued annotations (including $*/u$) to handle expansion-based and QCDCL-like calculi, offering a path toward broad, practical proof-checking pipelines for QBF solvers. Overall, the work bridges propositional and QBF proof complexity to support a unified certification approach with strong implications for solver verification and standardized checking formats.

Abstract

We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus, Long-Distance Q-Resolution, and Merge Resolution. These results are obtained by taking a technique of Beyersdorff et al. (JACM 2020) that turns strategy extraction into simulation and combining it with new local strategy extraction arguments. This approach leads to simulations that are carried out mainly in propositional logic, with minimal use of the QBF rules. Our proofs therefore provide a new, largely propositional interpretation of the simulated systems. We argue that these results strengthen the case for uniform certification in QBF solving, since many QBF proof systems now fall into place underneath extended QBF Frege.

Figures (5)

• Figure 1: Hasse diagram for polynomial simulation order of QBF calculi BCJ19BWJ14BBCP20HeuleSB17ChewSat21DBLP:journals/fmsd/BalabanovJ12Gelder12ChewHSAT22BBM18. In this diagram all proof systems below the first line are known to have strategy extraction, and all below the second line have an exponential lower bound. $\mathsf{G}$ and QRAT have strategy extraction if and only if $\mathsf{P}=\mathsf{PSPACE}$.
• Figure 2: The rules of $\forall$Exp+Res (adapted from JM15).
• Figure 3: The rules of IR-calcBCJ19.
• Figure 4: The rules of IRM-calcBCJ19.
• Figure 5: The rules of LQU$^+$- ResBWJ14.

Theorems & Definitions (70)

• Definition 3.1
• Definition 3.2
• Theorem 3.3
• proof : Proof of Theorem \ref{['thm:mrc']}
• Definition 4.1: BCJ19
• Definition 4.2: BCJ19
• Lemma 4.3
• Definition 4.4: Definition of resolvent policy for IR-calc
• Lemma 4.5
• proof