A Tough Nut for Tree Resolution

Authors

  • Stefan Dantchev
  • Søren Riis

DOI:

https://doi.org/10.7146/brics.v7i10.20137

Abstract

One of the earliest proposed hard problems for theorem provers is
a propositional version of the Mutilated Chessboard problem. It is well
known from recreational mathematics: Given a chessboard having two
diagonally opposite squares removed, prove that it cannot be covered with
dominoes. In Proof Complexity, we consider not ordinary, but 2n * 2n
mutilated chessboard. In the paper, we show a 2^Omega(n) lower bound for tree resolution.

Downloads

Published

2000-01-10

How to Cite

Dantchev, S., & Riis, S. (2000). A Tough Nut for Tree Resolution. BRICS Report Series, 7(10). https://doi.org/10.7146/brics.v7i10.20137