SOLVING AND GENERATING LARGE SUDOKU PUZZLES BY REDUCTION TO SAT

Abstract

Two problems related to Sudoku puzzles exist: the problem of solving and the problem of generating. In the most of the papers studying Sudoku, puzzles of size 9 x 9 are generated and solving methods are compared on these puzzles. The difference in solving times on these small-sized puzzles does not give a clear picture of the efficiency of different methods, as their solving times are measured in parts of the second. Few methods were developed for solving puzzles of greater size than 9 x 9: parallel solving, simulated annealing and method using probabilistic graphical models. We show that one well-known solving by reduction of Sudoku to SAT (Propositional satisfiability problem) significantly outperforms three mentioned methods. The main contribution of the paper is the improved existing algorithm for generating large and hard Sudoku puzzles – the property of the generated puzzles is uniqueness of the solution, and by removing any of the pre-filled numbers, this property is lost. We also evaluate the impact of the preprocessing rules (both in the process of solving and in the process of generating) used to deduce values of certain cells, prior to encoding to SAT. Preprocessing significantly speeds up the generating process but does not speed up solving of puzzles. We estimate the significance of the used rules and present some characteristics of the generated puzzles.