Stefan Dantchev1
Dept. of Mathematics and Computer Science, University
of Leicester dantchev@mcs.le.ac.uk
Søren Riis
Dept. of Computer Science, Queen Mary, University of London
smriis@dcs.qmw.ac.uk
Abstract:
We prove exponential lower bounds on the resolution proofs of some tautologies,
based on rectangular grid graphs. More specifically, we show a
lower bound for any resolution proof of the mutilated chessboard
problem on a
chessboard as well as for the Tseitin tautology based on the rectangular grid graph. The former result answers a 35 year old
conjecture by McCarthy.
lower bound for any resolution proof of the mutilated chessboard
problem on a 
chessboard as well as for the Tseitin tautology based on the 
rectangular grid graph. The former result answers a 35 year old
conjecture by McCarthy.