2013 IEEE International Symposium on Hardware-Oriented Security and Trust (HOST)
Download PDF

Abstract

We prove exponential lower bounds on the resolution proofs of some tautologies, based on rectangular grid graphs. More specifically, we show a 2^{\Omega (n)} lower bound for any resolution proof of the mutilated chessboard problem on a 2n × 2n chessboard as well as for the Tseitin tautology based on the n × n rectangular grid graph. The former result answers a 35 year old conjecture by McCarthy.
Like what you’re reading?
Already a member?
Get this article FREE with a new membership!

Similar Articles