Planar tautologies hard for resolution

Dantchev, Stefan; Riis, Soren

Abstract

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

Citation

Dantchev, S., & Riis, S. (2001, October). Planar tautologies hard for resolution. Presented at 42nd IEEE Symposium of Foundations of Computer Science, Las Vegas, Nev

• Presentation Conference Type: Conference Paper (published)
• Conference Name: 42nd IEEE Symposium of Foundations of Computer Science
• Publication Date: 2001-10
• Deposit Date: Feb 27, 2008
• Publicly Available Date: Nov 1, 2010
• Publisher: Institute of Electrical and Electronics Engineers
• Pages: 220-229
• Book Title: 42nd IEEE Symposium on Foundations of Computer Science, FOCS 2001, 14-17 October 2001, Las Vegas, Nevada ; proceedings.
• DOI: https://doi.org/10.1109/sfcs.2001.959896
• Public URL: https://durham-repository.worktribe.com/output/1698019