Home

Introduction

Sudoku is a number placement puzzle. The game consists of 9 X 9 grid i.e. 81 cells, each of which is to be filled with a digit out of set N = {1, 2, 3, 4, 5, 6, 7, 8, 9}.

Following is an example of an unsolved sudoku puzzle

The grid has a few cells filled and the player is expected to fill the remaining cells to reaach a valid solution. A valid solution must satisfy the following constraints :

• Each row must contain all the digits from N
• Each column must contain all the digits from N
• Each column must contain all the digits from N

The game of Sudoku can be modelled as an SAT problem ( explained below ). The main advantage of modelling the game as an SAT problem, is the inherent simplicity of the implementation.

Boolean Satisfiability Problem

Abbreviated as SAT problem is the problem of finding a valid assignment for the boolean literals in a given boolean expression such that it holds true. Boolean literals can assume a value ∈ B where B = {TRUE, FALSE}. For example -

Given the Boolean Expression: a AND NOT b, the problem is to "a" and "b" a value s.t. it the expression holds true. A solution to the above problem is clearly a = TRUE and b = FALSE.

Reference: Weber, Tjark. "A SAT-based Sudoku solver." LPAR. 2005