Sudoku solving using Z3.


 

Sudoku solving using Z3.

Program descriotion.

Downloads

Sudoku is a number puzzle. The objective is to fill a 9×9 grid so that each column, each row, and each of the nine 3×3 boxes (also called blocks or regions) contains the digits from 1 to 9 only one time each.  Some of the cells are filled initialy.

It is easy to introduce some variables, which correspond to numbers in cells, and write logic formulas with this variables, which describe the rules of this game. Such set of formulas and variables is called "theory" in mathematical logic. There are two possibilities:

  • This theory has a "model" (i.e. we can replace all variables by some numbers and satisfy all formulas by this replacing). Then this "model" is a sudoku solution.
  • This theory doesn't have a "model". Then there is no solution for this puzzle.

Obtained theory is simple, so we can entrust the job of model  construction to computer program, called SMT solver. The example of such program is Z3

 Here you can download programs, which illustrate this text and allows you to obtain z3 theories from given sudoku.  Then you can build a model using z3, and puzzle will be solved. Here is a short programs description.

I tested my program on difficult puzzles from here. The solving may take some time. Its amount depends on chosen approach, on puzzle complexity and your luck ;). While I use Bit Vectors it takes less than 1sec to solve. If I use Linear Arithmetic it takes 5-20sec. On some examples it takes up to 1-5min.You can read more about timing on program description page.

You can e-mail me on EpDmitry[at]yandex.ru.