On Proof Complexity for Quantified Boolean Formulas[HBNI Th112]

Abstract

Propositional proof complexity–a sub-branch of computational complexity–is an extensively studied area, with a number of lower bound techniques for various propositional proof systems (for example Resolution, and Cutting Planes). The purpose of this thesis is to assess whether similar techniques are applicable for proof systems for quantified Boolean formulas (QBFs). The major contributions of this work are as follows: 1. We show that level-ordered Q-resolution and tree-like Q-resolution, two restrictions of Q-resolution system, are incomparable. 2. We establish the feasible interpolation technique, first introduced by Krajıˇcek for Resolution [62], to all CDCL-based QBF Resolution calculi. This provides the first general lower bound method for CDCL-based QBF calculi and also extends the scope of the feasible interpolation technique. 3. We introduce a cutting planes system CP+∀red for QBFs and analyse the proof-theoretical strength of this new calculus. We also establish the strategy extraction technique and feasible interpolation technique for the new calculi. 4. We show that both the size-width relation, established by Ben-Sasson and Wigderson in [9], and space-width relation, established by Atserias and Dal- mau in [3], for the Resolution proof system drastically fail in Q-resolution, even in its weaker tree-like version.