• DocumentCode
    1710717
  • Title

    "Planar" tautologies hard for resolution

  • Author

    Dantchev, Stefan ; Riis, Soren

  • Author_Institution
    Dept. of Comput. Sci., Aarhus Univ., Denmark
  • fYear
    2001
  • Firstpage
    220
  • Lastpage
    229
  • Abstract
    We prove exponential lower bounds on the resolution proofs of some tautologies, based on rectangular grid graphs. More specifically, we show a 2Ω(n) lower bound for any resolution proof of the mutilated chessboard problem on a 2n×2n chessboard as well as for the Tseitin tautology (G. Tseitin, 1968) based on the n×n rectangular grid graph. The former result answers a 35 year old conjecture by J. McCarthy (1964).
  • Keywords
    computational complexity; graph theory; theorem proving; Tseitin tautology; exponential lower bounds; mutilated chessboard problem; planar tautologies; rectangular grid graph; rectangular grid graphs; resolution proofs; Bipartite graph; Computer science; Graph theory;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Foundations of Computer Science, 2001. Proceedings. 42nd IEEE Symposium on
  • Print_ISBN
    0-7695-1116-3
  • Type

    conf

  • DOI
    10.1109/SFCS.2001.959896
  • Filename
    959896
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1710717