Home

Browse
Communities
& Collections

Issue Date
Author
Title
Subject

Sign on to:

My Account
authorized users

Edit Profile

Help
 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 complexityexpander graphsresolutionres(k)automatizability 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: MasterDepartment of Computer Science - Master theses