Building a puzzle games solver using SAT solver

• Main Author: Nguyen Hung, Thai
• Other Authors: Alwen Fernanto Tiu
• Format: Final Year Project
• Language: English
• Published: 2017
• Subjects: DRNTU::Engineering::Computer science and engineering::Computing methodologies::Artificial intelligence
• Online Access: http://hdl.handle.net/10356/70184
• Institution: Nanyang Technological University

Solving puzzles such as Sudoku or The Eight Queens has long been a fascinating activity. In the last few decades, the birth of computer has played a significant role in exploring those puzzles; moreover, complete strategies for some of them has been found. Nonetheless, more complex puzzles which have exponential states are still challenging computer scientists with their struggling depth first search algorithms. For example, there is always a need for the Sudoku game’s creators to determine exactly whether their games are solvable, or if there existed unique solutions for them. Regrettably, the current backtracking method could not be fast enough, especially when the board size exceeds 10. Fortunately, satisfiability solver (SAT solver) risen recently has proved its ability to solve those enormous puzzles with a linear time complexity. SAT solver has clearly shown a strong potential in the field of strategy solving; therefore, scientists are in the search to expand the appliances of this new-but-promising technique. However, SAT solver has a major obstacle that prevents people from exploiting its powerful ability, that is, the difficulty in representing the puzzles’ rule in the form of conjunctive normal form (CNF), which is the standard input for SAT solver. In this project, a simple compiler was developed so as to transform the game’s rule into standard CNF, which is able to be solved by SAT solver then. Specifically, a language similar to First order logic is defined so that puzzles could be described in a more human readable form; subsequently, the compiler will convert the descriptions into CNF before letting SAT solver to solve them; finally, outputs of the SAT solver will then be transformed and represented as a normal board. Besides, the performance of the transformations as well as the solving process were also estimated, as a measurement in comparison to the traditional depth first search approach. In this project, three popular puzzles with different complexities, namely Sudoku, The N Queens and Rat in Maze, are used for the performance experiments. This report was written in order to discussed details of all the work, including statistics about the performance as well as evaluation and comment about them. Furthermore, possible improvements are mentioned so that in the future, the project could be perfectly finished and distributed as a useful tool for puzzle developers.