test Browse by Author Names Browse by Titles of Works Browse by Subjects of Works Browse by Issue Dates of Works

Advanced Search
& Collections
Issue Date   
Sign on to:   
Receive email
My Account
authorized users
Edit Profile   
About T-Space   

T-Space at The University of Toronto Libraries >
School of Graduate Studies - Theses >
Master >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1807/10444

Title: Expansion, Random Graphs and the Automatizability of Resolution
Authors: Zabawa, Daniel Michael
Advisor: Pitassi, Toniann
Department: Computer Science
Keywords: propositional proof complexity
expander graphs
Issue Date: 25-Jul-2008
Abstract: We explore the relationships between the computational problem of recognizing expander graphs, and the problem of efficiently approximating proof length in the well-known system of \emph{resolution}. This program builds upon known connections between graph expansion and resolution lower bounds. A proof system $P$ is \emph{(quasi-)automatizable} if there is a search algorithm which finds a $P$-proof of a given formula $f$ in time (quasi)polynomial in the length of a shortest $P$-proof of $f$. It is open whether resolution is (quasi-)automatizable. We prove several conditional non-automatizability results for resolution modulo new conjectures concerning the complexity of identifying bipartite expander graphs. Our reductions use a natural family of formulas and exploit the well-known relationships between expansion and length of resolution proofs. Our hardness assumptions are unsupported; we survey known results as progress towards establishing their plausibility. The major contribution is a conditional hardness result for the quasi-automatizability of resolution.
URI: http://hdl.handle.net/1807/10444
Appears in Collections:Master
Department of Computer Science - Master theses

Files in This Item:

File Description SizeFormat
Zabawa_Daniel_M_052008_MSc_thesis.pdf510.22 kBAdobe PDF

Items in T-Space are protected by copyright, with all rights reserved, unless otherwise indicated.