In previous post, I used python SAT solver to solve sudoku. Naturally, SV constraints are perfect to solve suduko once we figure out the correct constraints.

For Wiki, Sudoku is:

In classic Sudoku, the objective is to fill a 9 × 9 grid with digits so that each column, each row, and each of the nine 3 × 3 subgrids that compose the grid (also called “boxes”, “blocks”, or “regions”) contain all of the digits from 1 to 9.

It’s obvious we need 4 constraints(rows, cols and box) but the most important one is a constraint for each grid field.

Constraint 1 Link to heading

Using a quick loop and inside for each grid field.

constraint a19 {foreach (grid[i][j]) grid[i][j] inside {[1:9]}; }

Constraint 2 Link to heading

For rows, It’s easy to use unique on each row.

constraint rows {foreach(grid[i]) unique {grid[i][0:8]};}

Constraint 3 Link to heading

The columns are tricky. The solution i thought about is using nested loop and make sure that constraints on work with fields in other rows. seems to work.

constraint cols {
        foreach(grid[i,j]) {
            foreach(grid[r]) {
                (r != i) -> grid[i][j] != grid[r][j];
            }
        }
}

Constraint 4 Link to heading

The last one is unique box which is the hardest. Here the constrain works only on points in the same box. Note that index/3 returns the box for both x and y directions.

constraint box {
        foreach(grid[i,j]) {
            foreach(grid[x,y]) {
                (i != x && j != y && (i/3 == x/3) && (j/3 == y/3) ) -> grid[i][j] != grid[x][y];
            }
        }
}