Quantified Boolean Formulas (QBFs) extend propositional formulas with Boolean quantifiers. Working with QBF differs from propositional logic in its quantifier handling, but as propositional satisfiability (SAT) is a subproblem of QBF, all SAT hardness in solving and proof complexity transfers to QBF. This makes it difficult to analyse efforts dealing with “QBF hardness” specifically. In one response to this, Beyersdorff et. al. [18] created a framework for proof systems that allows us to factor out genuine QBF hardness from propositional hardness using oracles from the polynomial hierarchy.
Our work specifically deals with the most important case- when we use an NP oracle, removing any hardness due to propositional satisfiability in our proof systems.
The first results we present are re-examinations of the proof complexity landscape for QBF. Looking at the collapses of the QBF proof complexity simulation structure when including NP oracles. Some new simulations occur due to the NP oracles, in particular both universal resolution and weak extended variables are subsumed by the NP derivations. Some separations remain intact even with the NP-derivation rule such as the gap between expansion and QCDCL systems.
The NP-derivation rule allows us to say even more about QBF proof complexity. We show that QBF systems with general extension variables are incredibly powerful, and when adding in the NP-derivation rule, we can say something about its optimality and its use in practice. In Jussila et. al [31] Extended Q-Res was put forward as reasonable calculus for a universal proof checking of solver. We here justify that partially through theory. We find that, with the NP derivation rule, general extended QU-Res achieves an optimality result simulating all QBF proof systems as long as they have strategy extraction.