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.
| Identifer | oai:union.ndltd.org:TORONTO/oai:tspace.library.utoronto.ca:1807/10444 |
| Date | 25 July 2008 |
| Creators | Zabawa, Daniel Michael |
| Contributors | Pitassi, Toniann |
| Source Sets | University of Toronto |
| Language | en_ca |
| Detected Language | English |
| Type | Thesis |
| Format | 522468 bytes, application/pdf |
Page generated in 0.0015 seconds