Lower Bound Techniques for QBF Expansion

Abstract

We propose some general techniques for proving lower bounds in expansion-based QBF proof systems. We present them in a framework centred on natural properties of winning strategies in the ‘evaluation game’ interpretation of QBF semantics. As applications, we prove an exponential proof-size lower bound for a whole class of formula families, and demonstrate the power of our approach over existing methods by providing alternative short proofs of two known hardness results. We also use our technique to deduce an interesting result: in the absence of propositional hardness, formulas separating the two major QBF expansion systems must have unbounded quantifier alternations.