Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution

We provide a tight characterisation of proof size in resolution for quantified Boolean formulas (QBF) by circuit complexity. Such a characterisation was previously obtained for a hierarchy of QBF Frege systems (Beyersdorff & Pich, LICS 2016), but leaving open the most important case of QBF resolution. Different from the Frege case, our characterisation uses a new version of decision lists as its circuit model, which is stronger than the CNFs the system works with. Our decision list model is well suited to compute countermodels for QBFs.

Our characterisation works for both Q-Resolution and QU-Resolution, which we show to be polynomially equivalent for QBFs of bounded quantifier alternation.

Using our characterisation we obtain a size-width relation for QBF resolution in the spirit of the celebrated result for propositional resolution (Ben-Sasson & Wigderson, J. ACM 2001). However, our result is not just a replication of the propositional relation -intriguingly ruled out for QBF in previous research (Beyersdorff et al., ACM ToCL 2018)but shows a different dependence between size, width, and quantifier complexity.

We demonstrate that our new technique elegantly reproves known QBF hardness results and unifies previous lower-bound techniques in the QBF domain.