How to Solve a Sudoku - A logical analysis and algorithmic implementation of strategically Solving Sudoku puzzles

Abstract

Sudokus are widely popular logical combinatorial puzzles. From the Sunday newspaper to World Championships, many people like to take a crack at the worldfamous puzzle. Many sudoku solvers exist, often based on efficiency and therefore not taking human thinking steps and strategies into account. Consequently, there is currently not a solver which can logically explain its steps. Something which would be useful to aid human players in their own solving process. Therefore the aim of this thesis is to answer whether it is possible to build a transparent logical algorithm which solves sudoku’s based on human strategies, by analysing the logic behind these strategies. And if this is the case, what would such a solver look like? Because of this the aim of the thesis is twofold, consisting of a logical analysis and an algorithmic implementation. The Sudoku puzzle is formalized as a Modal Logic Problem. To approximate how human puzzlers complete Sudokus, thirteen of the most popular Sudoku solving strategies are gathered and formalized as Alethic Natural Deduction rules and their dependency and complexity is analysed. Based on this Helping HAND, a Heuristic Alethic Natural Deduction based Sudoku solver, is proposed. Helping HAND searches for optimal strategies by Weighted Graph Search and can solve Sudokus while being able to explain each step along the way. This algorithm proves to be a valuable step in the field of explainable AI.