Automatic Solutions of Logic Puzzles

Thesis advisor: Howard StraubingThe use of computer programs to automatically solve logic puzzles is examined in this work. A typical example of this type of logic puzzle is one in which there are five people, with five different occupations and five different color houses. The task is to use various clues to determine which occupation and which color belongs to each person. The clues to this type of puzzle often are statements such as, ''John is not the barber,'' or ''Joe lives in the blue house.'' These puzzles range widely in complexity with varying numbers of objects to identify and varying numbers of characteristics that need to be identified for each object. With respect to the theoretical aspects of solving these puzzles automatically, this work proves that the problem of determining, given a logic puzzle, whether or not that logic puzzle has a solution is NP-Complete. This implies, provided that P is not equal to NP, that, for large inputs, automated solvers for these puzzles will not be efficient in all cases. Having proved this, this work proceeds to seek methods that will work for solving these puzzles efficiently in most cases. To that end, each logic puzzle can be encoded as an instance of boolean satisfiability. Two possible encodings are proposed that both translate logic puzzles into boolean formulas in Conjunctive Normal Form. Using a selection of test puzzles, a group of boolean satisfiability solvers is used to solve these puzzles in both encodings. In most cases, these simple solvers are successful in producing solutions efficiently.Thesis (BS) — Boston College, 2009.Submitted to: Boston College. College of Arts and Sciences.Discipline: College Honors Program.Discipline: Computer Science