You end up with three symmetric constraints + the box constraint:
- The sum along any x, y, or z row is 1 (one of each number per row, one of each number per column, and one number per square)
- The sum of each 3x3x1 box slice is 1 (one of each number per box)
I really like the symmetry between the row sum constraints here. And it does pretty neatly align with the way many people solve Sudoku by writing little numbers in the squares to represent possible values before pruning impossible ones.
A full MiniZinc program would look like this
int: n = 3;
int: s = n*n;
set of int: S = 1..s;
array[S, S] of opt S: puzzle;
array[S, S] of var S: board;
% Sudoku constraints
constraint forall(row in S) ( all_different(board[row, ..]) );
constraint forall(col in S) ( all_different(board[.., col]) );
constraint forall(r, c in {1, 4, 7}) (
all_different(board[r..<r+n, c..<c+n])
);
% Set up puzzle
constraint forall (r, c in S where occurs(puzzle[r, c])) (
board[r, c] = puzzle[r, c]
);
solve satisfy;
And an instance file looks like this puzzle = [|
9, <>, 8, 1, <>, <>, <>, <>, 4 |
1, 2, <>, <>, 8, 6, <>, 5, <> |
<>, <>, 7, <>, <>, <>, <>, 1, <> |
<>, 8, 3, <>, <>, <>, <>, 6, 9 |
7, <>, 6, 8, <>, 3, <>, <>, <> |
<>, <>, <>, 4, 6, <>, <>, 8, <> |
<>, <>, <>, <>, <>, 1, <>, <>, <> |
<>, <>, <>, <>, <>, 4, 5, <>, 1 |
5, 4, 1, 9, 3, 8, <>, <>, <>
|];
MontagFTB•3mo ago
mzl•3mo ago
While 9x9 Sudoku problems are trivial to solve for more or less any program, 25x25 Sudoku instances are quite tricky and a simple and fast but naive search for a solution can easily take hours.
pdwetz•3mo ago
mzl•3mo ago
For pen-and-paper puzzles like Sudoku there is usually the goal that a solution should be findable by a series of deductive steps. For 9x9 Sudoku, most deductive steps used correspond to the effects well-known propagation techniques offer[1]. With a suitable propagation level, if the puzzle is solved search-free, then one knows that both there is only one solution and that there is a deductive path to solve it.
[1]: See "Sudoku as a Constraint Problem", Helmut Simonis, https://ai.dmi.unibas.ch/_files/teaching/fs21/ai/material/ai... for some data on 9x9 Sudoku difficulty and the propagation techniques that are needed for search-free solving.