"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).

Authors

• Stefan S. Dantchev
• Søren Riis

Keywords

• Computer science
• Bipartite graph
• Graph theory
• Lower Bound
• Grid Graph
• Deterministic
• Vertices
• Flow Values
• Number Of Squares
• Incoming Edges
• Components Of The Graph
• Round Of The Game
• Real Game
• Flat Wall
• Empty Squares