Reasons for Hardness in QBF Proof Complexity

Quantified Boolean Formulas (QBF) extend the canonical NP-complete satisfiability problem by including Boolean quantifiers. Determining the truth of a QBF is PSPACE-complete; this is expected to be a harder problem than satisfiability, and hence QBF solving has much wider applications in practice. QBF proof complexity forms the theoretical basis for understanding QBF solving, as well as providing insights into more general complexity theory, but is less well understood than propositional proof complexity. We begin this thesis by looking at the reasons underlying QBF hardness, and in particular when the hardness is propositional in nature, rather than arising due to the quantifiers. We introduce relaxing QU-Res, a previous model for identifying such propositional hardness, and construct an example where relaxing QU-Res is unsuccessful in this regard. We then provide a new model for identifying such hardness which we prove captures this concept. Now equipped with a means of identifying ‘genuine’ QBF hardness, we prove a new lower bound technique for tree-like QBF proof systems. Lower bounds using this technique allows us to show a new separation between tree-like and dag-like systems. We give a characterisation of lower bounds for a large class of tree-like proof systems, in which such lower bounds play a prominent role. Further to the tree-like bound, we provide a new lower bound technique for QBF proof systems in general. This technique has some similarities to the above technique for tree-like systems, but requires some refinement to provide bounds for dag-like systems. We give applications of this new technique by proving lower bounds across several systems. The first such lower bounds are for a very simple family of QBFs. We then provide a construction to combine false QBFs to give formulas for which we can show lower bounds in this way, allowing the generation of the first random QBF proof complexity lower bounds.