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:
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 520sec. On some examples it takes up to 15min.You can read more about timing on program description page. You can email me on EpDmitry[at]yandex.ru.
