Use this resource - and many more! - in your textbook!
AcademicPub holds over eight million pieces of educational content for you to mix-and-match your way.
"Planar" tautologies hard for resolution
By: Dantchev, S.; Riis, S.;
2001 / IEEE / 0-7695-1116-3
This item was taken from the IEEE Conference ' "Planar" tautologies hard for resolution ' We prove exponential lower bounds on the resolution proofs of some tautologies, based on rectangular grid graphs. More specifically, we show a 2/sup /spl Omega/(n)/ lower bound for any resolution proof of the mutilated chessboard problem on a 2n/spl times/2n chessboard as well as for the Tseitin tautology (G. Tseitin, 1968) based on the n/spl times/n rectangular grid graph. The former result answers a 35 year old conjecture by J. McCarthy (1964).