How to specify that in every row and in every column and in every three times three

block exactly the numbers one to nine occur all exactly once?

Again, this can be done in several ways.

We chose to specify that these numbers are all at least one and at most nine,

and they are all distinct.

Then the next question is,

how to express that the number of numbers is distinct?

Well, we could do it directly.

Simply, for every pair,

write down that they are different, not equal.

But the SMT syntax also has a special construct called distinct and that can be

used by just writing down distinct and then the variables that should be distinct.

Doing so is very straightforward.

We start by declaring the variable.

Well, in fact, we only have one function to be

declared depending on two integers and the result is also an integer.

Next, we have the requirements by and assert,

and what are the requirements?

Well, all values should be greater or equal 1,

and less or equal than 9.

Here it's specified for A 1 1,

but it's similar for all other IAGA running from one to nine.

And next, the elements in a row,

let's say row one should be distinct,

and that is described by this formula.

And similar for the other rows,

and similar for every column,

and similar for every three times three block.

Like distinct and here we see

the elements of the upper most leftmost three by three block.

And then the full formula is concluded by the given numbers in the Sudoku puzzle.

On position one three row one column three,

there was nine, so we simply gave that that value should be nine.

And for one four it should be eight and so on.

This we do for all given numbers in the Sudoku puzzle.

And now applying the set 3 or any other SMT solver on the resulting formula,

yields a satisfying assignment giving the values for

all variables being the solutions of the Sudoku puzzle and this hardly takes time,

it's within a fraction of a second.

Here we see the puzzle as it was given,

and if we fill in the values as they were found by the SMT solver,

we get these values and indeed you can check that everything is okay.

So, this is a solution of this puzzle

found in the fraction of a second while for a human,

this is a hard job.

Great part of the formula is the same for all Sudoku puzzles.

Namely, the value shoot in between one and nine,

and in every row,

column and block the values should be distinct.

And the rest of the formula just specifies the values given in the Sudoku puzzle.

And in this way, we can quickly solve

all Sudoku puzzle as you find them in newspapers or whatever.