Hall 123

On Proof Complexity for Quantified Boolean Formulas

Anil Shukla

IMSc

HBNI PhD Thesis defense

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 CuttingPlanes). 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 Krajicek for Resolution in 1997, 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+\forall~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 2001, and the space-width relation, established by Atserias and Dalmau in 2008, in Resolution proof system drastically fail in Q-resolution, even in its weaker tree-like version.