Mutilated chessboard problem
The mutilated chessboard problem is a tiling puzzle proposed by philosopher Max Black in his book Critical Thinking (1946). It was later discussed by Solomon W. Golomb (1954), Gamow & Stern (1958) or by Martin Gardner in his Scientific American column "Mathematical Games." The problem is as follows:
Most considerations of this problem in literature provide solutions "in the conceptual sense" without proofs. John McCarthy proposed it as a hard problem for automated proof systems. In fact, its solution using the resolution system of inference is exponentially hard.
The puzzle is impossible to complete. A domino placed on the chessboard will always cover one white square and one black square. Therefore, a collection of dominoes placed on the board will cover an equal numbers of squares of each colour. If the two white corners are removed from the board then 30 white squares and 32 black squares remain to be covered by dominoes, so this is impossible. If the two black corners are removed instead, then 32 white squares and 30 black squares remain, so it is again impossible. 
The same impossibility proof shows that no domino tiling exists whenever any two white squares are removed from the chessboard. However, if two squares of opposite colors are removed, then it is always possible to tile the remaining board with dominoes; this result is called Gomory's theorem, and is named after mathematician Ralph E. Gomory, whose proof was published in 1973. Gomory's theorem can be proven using a Hamiltonian cycle of the grid graph formed by the chessboard squares; the removal of two oppositely-colored squares splits this cycle into two paths with an even number of squares each, both of which are easy to partition into dominoes.
- Andrews, Peter B.; Bishop, Matthew (1996), "On Sets, Types, Fixed Points, and Checkerboards", Theorem Proving With Analytic Tableaux and Related Methods: 5th International Workshop, Tableaux '96, Terrasini, Palermo, Italy, 15-17th, 1996, Proceedings, Lecture Notes in Computer Science, Springer-Verlag,
most treatments of the problem in the literature solve it in the conceptual sense, but do not actually provide proofs of the theorem in either of McCarthy's original formulations.
- Bancerek, Grzegorz (1995), "The Mutilated Chessboard Problem—checked by Mizar", in Boyer, Robert; Trybulec, Andrzej, QED Workshop, II, Warsaw University, pp. 25–26,
The problem presented by John McCarthy during his lecture "Heavy duty set theory"1 has been resolved here.
- Arthan, R. D. (2005), The Mutilated Chessboard Theorem in Z (PDF), retrieved 2007-05-06,
The mutilated chessboard theorem was proposed over 40 years ago by John McCarthy as a “tough nut to crack” for automated reasoning.
- Alekhnovich, Michael (2004), "Mutilated chessboard problem is exponentially hard for resolution", Theoretical Computer Science 310 (1-3): 513–525, doi:10.1016/S0304-3975(03)00395-5.
- McCarthy, John (1999), "Creative Solutions to Problems", AISB Workshop on Artificial Intelligence and Creativity, retrieved 2007-04-27
- Watkins, John J. (2004), Across the board: the mathematics of chessboard problems, Princeton University Press, pp. 12–14, ISBN 978-0-691-11503-0.
- According to Mendelsohn, the original publication is in Honsberger's book. Mendelsohn, N. S. (2004), "Tiling with dominoes", The College Mathematics Journal (Mathematical Association of America) 35 (2): 115–120, doi:10.2307/4146865, JSTOR 4146865; Honsberger, R. (1973), Mathematical Gems I, Mathematical Association of America.
- Gamow, George; Stern, Marvin (1958), Puzzle-Math, Viking Press, ISBN 978-0-333-08637-7
- Gardner, Martin (1994), My Best Mathematical and Logic Puzzles, Dover, ISBN 0-486-28152-3
|Wikimedia Commons has media related to Mutilated chessboard problem.|