On Proof Complexity for Quantified Boolean Formulas[HBNI Th112]

DSpace/Manakin Repository

On Proof Complexity for Quantified Boolean Formulas[HBNI Th112]

Show simple item record

dc.contributor.author Anil Shukla
dc.date.accessioned 2017-05-16T07:10:58Z
dc.date.available 2017-05-16T07:10:58Z
dc.date.issued 2017-05-16T07:10:58Z
dc.date.submitted 2017
dc.identifier.uri http://hdl.handle.net/123456789/399
dc.description.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. en_US
dc.publisher.publisher
dc.subject QBF Proof Systems en_US
dc.subject Quantified Boolean Formulas en_US
dc.subject HBNI Th112 en_US
dc.title On Proof Complexity for Quantified Boolean Formulas[HBNI Th112] en_US
dc.type.degree Ph.D en_US
dc.type.institution HBNI en_US
dc.description.advisor Meena Mahajan
dc.description.pages 141p. en_US
dc.type.mainsub Computer Science en_US

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 simple item record

Search DSpace


Advanced Search

Browse

My Account