Planar tautologies hard for resolution

Dantchev, Stefan; Riis, Soren

doi:10.1109/sfcs.2001.959896

Planar tautologies hard for resolution

Dantchev, Stefan; Riis, Soren

Authors

Dr Stefan Dantchev s.s.dantchev@durham.ac.uk
Assistant Professor

Soren Riis

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). Planar tautologies hard for resolution. In 42nd IEEE Symposium on Foundations of Computer Science, FOCS 2001, 14-17 October 2001, Las Vegas, Nevada ; proceedings (220-229). https://doi.org/10.1109/sfcs.2001.959896

Conference Name	42nd IEEE Symposium of Foundations of Computer Science
Conference Location	Las Vegas, Nev
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

Files

Published Conference Proceeding (233 Kb)
PDF

Copyright Statement
© 2001 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.