next up previous
Next: About this document ...

``Planar'' tautologies, hard for Resolution

Stefan Dantchev1
Dept. of Mathematics and Computer Science, University of Leicester
Søren Riis
Dept. of Computer Science, Queen Mary, University of London


We prove exponential lower bounds on the resolution proofs of some tautologies, based on rectangular grid graphs. More specifically, we show a $2^{\Omega \left(n\right)}$ lower bound for any resolution proof of the mutilated chessboard problem on a $2n\times 2n$ chessboard as well as for the Tseitin tautology based on the $n\times n$ rectangular grid graph. The former result answers a 35 year old conjecture by McCarthy.

S. Dantchev 2002-12-11