1 6 2 4 5 hole 3 8 9 10 7 11 13 14 15 12
Fifteen tiles, numbered from 1 through 15, rest in a four by four tray. The tiles can be slid up, down, left, or right, provided that the "hole" allows the move. The goal is to achieve the following:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 hole
Question:
Assume that the numbered tiles are in a scrambled arrangement, for example, the following:
1 6 2 4 5 hole 3 8 9 10 7 11 13 14 15 12
Can they be slid up, down, left, right until they are back in order as shown in the diagram?
Solution: This puzzle has been solved.
We present the puzzle here as an example of some of the challenges one faces in representing implicit as well as explicit information to an automated reasoning program.
A detailed discussion of this puzzle and others is given in Automated Reasoning: Introduction and Applications, by Larry Wos, Ross Overbeek, Ewing Lusk, and Jim Boyle. The book, published by McGraw-Hill, includes a diskette of the automated reasoning program OTTER, which can be used to solve puzzles as well as extremely challenging problems in mathematics and logic.
Those who have OTTER already may simply use the chosen clauses and start experimenting.