On Proof Complexity for Quantified Boolean Formulas[HBNI Th112]

DSpace/Manakin Repository

On Proof Complexity for Quantified Boolean Formulas[HBNI Th112]

Show full item record

Title: On Proof Complexity for Quantified Boolean Formulas[HBNI Th112]
Author: Anil Shukla
Advisor: Meena Mahajan
Degree: Ph.D
Main Subjects: Computer Science
Institution: HBNI
Year: 2017
Pages: 141p.
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.
URI: http://hdl.handle.net/123456789/399

Files in this item

Files Size Format View
HBNI Th112.pdf 902.2Kb PDF View/Open

This item appears in the following Collection(s)

Show full item record

Search DSpace


Advanced Search

Browse

My Account