The mutilated chessboard problem is a tiling puzzle posed by Max Black in 1946 that asks:
Suppose a standard 8×8 chessboard (or checkerboard) has two diagonally opposite corners removed, leaving 62 squares. Is it possible to place 31 dominoes of size 2×1 so as to cover all of these squares?
It is an impossible puzzle: there is no domino tiling meeting these conditions. One proof of its impossibility uses the fact that, with the corners removed, the chessboard has 32 squares of one color and 30 of the other, but each domino must cover equally many squares of each color. More generally, if any two squares are removed from the chessboard, the rest can be tiled by dominoes if and only if the removed squares are of different colors. This problem has been used as a test case for automated reasoning, creativity, and the philosophy of mathematics.
The mutilated chessboard problem is an instance of domino tiling of grids and polyominoes, also known as "dimer models", a general class of problems whose study in statistical mechanics dates to the work of Ralph H. Fowler and George Stanley Rushbrooke in 1937. [1] Domino tilings also have a long history of practical use in pavement design and the arrangement of tatami flooring. [2]
The mutilated chessboard problem itself was proposed by philosopher Max Black in his book Critical Thinking (1946), with a hint at the coloring-based solution to its impossibility. [3] [4] It was popularized in the 1950s through later discussions by Solomon W. Golomb (1954), [5] George Gamow and Marvin Stern (1958), [6] Claude Berge (1958), [4] [7] and Martin Gardner in his Scientific American column "Mathematical Games" (1957). [8]
The use of the mutilated chessboard problem in automated reasoning stems from a proposal for its use by John McCarthy in 1964. [9] [10] It has also been studied in cognitive science as a test case for creative insight, [11] [12] [13] Black's original motivation for the problem. [3] In the philosophy of mathematics, it has been examined in studies of the nature of mathematical proof. [14] [15] [16] [17]
The puzzle is impossible to complete. A domino placed on the chessboard will always cover one white square and one black square. Therefore, any collection of dominoes placed on the board will cover equal numbers of squares of each color. But any two opposite squares have the same color: both black or both white. If they are removed, there will be fewer squares of that color and more of the other color, making the numbers of squares of each color unequal and the board impossible to cover. [8] The same idea shows that no domino tiling can exist whenever any two squares of the same color (not just the opposite corners) are removed from the chessboard. [18]
Several other proofs of impossibility have also been found. A proof by Shmuel Winograd starts with induction. In a given tiling of the board, if a row has an odd number of squares not covered by vertical dominoes from the previous row, then an odd number of vertical dominoes must extend into the next row. The first row trivially has an odd number of squares (namely, 7) not covered by dominoes of the previous row. Thus, by induction, each of the seven pairs of consecutive rows houses an odd number of vertical dominoes, producing an odd total number. By the same reasoning, the total number of horizontal dominoes must also be odd. As the sum of two odd numbers, the total number of dominoes—vertical and horizontal—must be even. But to cover the mutilated chessboard, 31 dominoes are needed, an odd number. [19] [20] Another method counts the edges of each color around the boundary of the mutilated chessboard. Their numbers must be equal in any tileable region of the chessboard, because each domino has three edges of each color, and each internal edge between dominoes pairs off boundaries of opposite colors. However, the mutilated chessboard has more edges of one color than the other. [21]
If two squares of opposite colors are removed, then the remaining board can always be tiled with dominoes; this result is Gomory's theorem, [22] after mathematician Ralph E. Gomory, whose proof was published in 1973. [18] [20] Gomory's theorem can be proven using a Hamiltonian cycle of the grid graph formed by the chessboard squares. The removal of any two oppositely colored squares splits this cycle into two paths with an even number of squares each. Both of these paths are easy to partition into dominoes by following them. [22] Gomory's theorem is specific to the removal of only one square of each color. Removing larger numbers of squares, with equal numbers of each color, can result in a region that has no domino tiling, but for which coloring-based impossibility proofs do not work. [23]
Domino tiling problems on polyominoes, such as the mutilated chessboard problem, can be solved in polynomial time, either by converting them into problems in group theory, [21] [24] or as instances of bipartite matching. In the latter formulation, one obtains a bipartite graph with a vertex for each available chessboard square and an edge for every pair of adjacent squares; the problem is to find a system of edges that touches each vertex exactly once. As in the coloring-based proof of the impossibility of the mutilated chessboard problem, the fact that this graph has more vertices of one color than the other implies that it fails the necessary conditions of Hall's marriage theorem, so no matching exists. [23] [25] [26] The problem can also be solved by formulating it as a constraint satisfaction problem, and applying semidefinite programming to a relaxation. [27]
In 1964, John McCarthy proposed the mutilated chessboard as a hard problem for automated proof systems, formulating it in first-order logic and asking for a system that can automatically determine the unsolvability of this formulation. [9] Most considerations of this problem provide solutions "in the conceptual sense" that do not apply to McCarthy's logic formulation of the problem. [28] Despite the existence of general methods such as those based on graph matching, it is exponentially hard for resolution to solve McCarthy's logical formulation of the problem, [29] [30] [31] highlighting the need for methods in artificial intelligence that can automatically change to a more suitable problem representation [32] and for knowledge representation systems that can manage the equivalences between different representations. [10] Short proofs are possible using resolution with additional variables, [33] or in stronger proof systems allowing the expression of avoidable tiling patterns that can prune the search space. [34] Higher-level proof assistants are capable of handling the coloring-based impossibility proof directly; these include Isabelle, [35] the Mizar system, [36] and Nqthm. [37]
A similar problem asks if a wazir starting at a corner square of an ordinary chessboard can visit every square exactly once, and finish at the opposite corner square. The wazir is a fairy chess piece that can move only one square vertically or horizontally (not diagonally). Using similar reasoning to the mutilated chessboard problem's classic solution, this wazir's tour does not exist. For example, if the initial square is white, as each move alternates between black and white squares, the final square of any complete tour is black. However, the opposite corner square is white. [38] This sort of tour of a chessboard also forms the basis of a type of puzzle called Numbrix, which asks for a tour in which the positions of certain squares match given clues. [39] The impossibility of a corner-to-corner tour shows the impossibility of a Numbrix puzzle with the clues 1 in one corner and 64 in the opposite corner.
De Bruijn's theorem concerns the impossibility of packing certain cuboids into a larger cuboid. For instance, it is impossible, according to this theorem, to fill a 6 × 6 × 6 box with 1 × 2 × 4 cuboids. The proof uses a similar chessboard-coloring argument to the mutilated chessboard problem. [40]
In mathematics, the four color theorem, or the four color map theorem, states that no more than four colors are required to color the regions of any map so that no two adjacent regions have the same color. Adjacent means that two regions share a common boundary of non-zero length. It was the first major theorem to be proved using a computer. Initially, this proof was not accepted by all mathematicians because the computer-assisted proof was infeasible for a human to check by hand. The proof has gained wide acceptance since then, although some doubts remain.
A tetromino is a geometric shape composed of four squares, connected orthogonally. Tetrominoes, like dominoes and pentominoes, are a particular type of polyomino. The corresponding polycube, called a tetracube, is a geometric shape composed of four cubes connected orthogonally.
Wang tiles, first proposed by mathematician, logician, and philosopher Hao Wang in 1961, are a class of formal systems. They are modelled visually by square tiles with a color on each side. A set of such tiles is selected, and copies of the tiles are arranged side by side with matching colors, without rotating or reflecting them.
A polyomino is a plane geometric figure formed by joining one or more equal squares edge to edge. It is a polyform whose cells are squares. It may be regarded as a finite subset of the regular square tiling.
A mathematical proof is a deductive argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proof can, in principle, be constructed using only certain basic or original assumptions known as axioms, along with the accepted rules of inference. Proofs are examples of exhaustive deductive reasoning which establish logical certainty, to be distinguished from empirical arguments or non-exhaustive inductive reasoning which establish "reasonable expectation". Presenting many cases in which the statement holds is not enough for a proof, which must demonstrate that the statement is true in all possible cases. A proposition that has not been proved but is believed to be true is known as a conjecture, or a hypothesis if frequently used as an assumption for further mathematical work.
In mathematics, parity is the property of an integer of whether it is even or odd. An integer is even if it is divisible by 2, and odd if it is not divisible. For example, −4, 0, and 82 are even numbers, while −3, 5, 7, and 21 are odd numbers.
A checkerboard or chequerboard is a board of checkered pattern on which checkers is played. Most commonly, it consists of 64 squares (8×8) of alternating dark and light color, typically green and buff, black and red, or black and white. An 8×8 checkerboard is used to play many other games, including chess, whereby it is known as a chessboard. Other rectangular square-tiled boards are also often called checkerboards.
The Black Path Game is a two-player board game described and analysed in Winning Ways for your Mathematical Plays. It was invented by Larry Black in 1960.
A tromino or triomino is a polyomino of size 3, that is, a polygon in the plane made of three equal-sized squares connected edge-to-edge.
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.
Tiling puzzles are puzzles involving two-dimensional packing problems in which a number of flat shapes have to be assembled into a larger given shape without overlaps. Some tiling puzzles ask players to dissect a given shape first and then rearrange the pieces into another shape. Other tiling puzzles ask players to dissect a given shape while fulfilling certain conditions. The two latter types of tiling puzzles are also called dissection puzzles.
A computer-assisted proof is a mathematical proof that has been at least partially generated by computer.
In graph theory, a rook's graph is an undirected graph that represents all legal moves of the rook chess piece on a chessboard. Each vertex of a rook's graph represents a square on a chessboard, and there is an edge between any two squares sharing a row (rank) or column (file), the squares that a rook can move between. These graphs can be constructed for chessboards of any rectangular shape. Although rook's graphs have only minor significance in chess lore, they are more important in the abstract mathematics of graphs through their alternative constructions: rook's graphs are the Cartesian product of two complete graphs, and are the line graphs of complete bipartite graphs. The square rook's graphs constitute the two-dimensional Hamming graphs.
In graph theory, a branch of mathematics, the handshaking lemma is the statement that, in every finite undirected graph, the number of vertices that touch an odd number of edges is even. For example, if there is a party of people who shake hands, the number of people who shake an odd number of other people's hands is even. The handshaking lemma is a consequence of the degree sum formula, also sometimes called the handshaking lemma, according to which the sum of the degrees equals twice the number of edges in the graph. Both results were proven by Leonhard Euler in his famous paper on the Seven Bridges of Königsberg that began the study of graph theory.
In geometry, a domino tiling of a region in the Euclidean plane is a tessellation of the region by dominoes, shapes formed by the union of two unit squares meeting edge-to-edge. Equivalently, it is a perfect matching in the grid graph formed by placing a vertex at the center of each square of the region and connecting two vertices when they correspond to adjacent squares.
An edge-matching puzzle is a type of tiling puzzle involving tiling an area with polygons whose edges are distinguished with colours or patterns, in such a way that the edges of adjacent tiles match.
In combinatorial mathematics, an Aztec diamond of order n consists of all squares of a square lattice whose centers (x,y) satisfy |x| + |y| ≤ n. Here n is a fixed integer, and the square lattice consists of unit squares with the origin as a vertex of 4 of them, so that both x and y are half-integers.
In mathematics, a domino is a polyomino of order 2, that is, a polygon in the plane made of two equal-sized squares connected edge-to-edge. When rotations and reflections are not considered to be distinct shapes, there is only one free domino.
Polyominoes: Puzzles, Patterns, Problems, and Packings is a mathematics book on polyominoes, the shapes formed by connecting some number of unit squares edge-to-edge. It was written by Solomon Golomb, and is "universally regarded as a classic in recreational mathematics". The Basic Library List Committee of the Mathematical Association of America has strongly recommended its inclusion in undergraduate mathematics libraries.
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