Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Mutilated chessboard problem is exponentially hard for resolution
Alekhnovich M. Theoretical Computer Science310 (1-3):513-525,2004.Type:Article
Date Reviewed: Apr 1 2004

Simple problems that resist routine logic tempt one to waste time. Often, a clever idea makes a result obvious, but a formal proof takes time and space.

This note presents a new result on a well-known “tough nut.” The “nut” is the placing of dominoes on a chess board with two opposite corner squares missing. Each square has half a domino. Each domino covers two adjacent squares. I have used this problem with undergraduate computer science students. They, with a little prompting, prove that it is impossible. The author examines proof techniques used in artificial intelligence and logic programming. He proves an exponential lower bound for the size of these proofs. While reading this note, I tackled the four-by-four case by hand, using a semantic tableau, and using Prolog. The results were consistent with his lower bound.

The note presents another obvious result with a convoluted proof. The author’s bound seems obvious given the tighter bound he quotes[1]. Nevertheless, he presents a clever and intricate proof. It reduces the chess board problem to the construction of an infinite roadway of four-by-four tilings of the chess board. His proof techniques seem novel. They would benefit from a longer exposition. A long proof of a known result only deserves a short note, however.

Only proof theory professionals should study this note.

Reviewer:  Richard Botting Review #: CR129370 (0409-1085)
1) Dantchev, S, Riis, S, A tough nut for tree resolution. RS-00-10 BRICS: Basic Research in Computer Science, Aarhus. 2000 http://www.brics.dk/RS/00/10/.
1) Dantchev, S, Riis, S, A tough nut for tree resolution. RS-00-10 BRICS: Basic Research in Computer Science, Aarhus. 2000, http://www.brics.dk/RS/00/10/.
Bookmark and Share
  Reviewer Selected
Featured Reviewer
 
 
Computational Logic (F.4.1 ... )
 
 
Complexity Of Proof Procedures (F.2.2 ... )
 
 
Deduction And Theorem Proving (I.2.3 )
 
 
Discrete Mathematics (G.2 )
 
Would you recommend this review?
yes
no
Other reviews under "Computational Logic": Date
Extended Horn sets in propositional logic
Chandru V., Hooker J. Journal of the ACM 38(1): 205-221, 1991. Type: Article
Nov 1 1991
Preservation of expressive completeness in temporal models
Amir A., Gabbay D. (ed)   (,1991. Type: Proceedings
Oct 1 1987
Monotone versus positive
Ajtai M., Gurevich Y. (ed) Journal of the ACM 34(4): 1004-1015, 1987. Type: Article
Jul 1 1988
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy