Greater-than Sudoku in MiniZinc
Greater-than Sudoku is like an ordinary Sudoku puzzle, but the number clues are replaced with less-than and greater-than relations.
Sergii Dymchenko showed how to solve it with ECLiPSe, and Hakan Kjellerstrand translated that to Picat, so I couldn’t resist trying to model it in MiniZinc.
array[int,int] of string : horizontal;
array[int,int] of string : vertical;
horizontal =
[| ">","<",">","<","<",">",
| ">","<","<","<",">",">",
| "<",">","<",">",">","<",
| ">","<",">","<","<","<",
| "<","<","<",">",">","<",
| ">",">",">","<","<",">",
| ">",">","<",">",">","<",
| "<",">","<",">","<",">",
| "<",">",">","<","<",">" |];
vertical =
[| "^","v","^","v","v","^","^","^","^"
| "v","^","^","^","^","v","^","v","^"
| "v","^","^","v","^","v","^","v","v"
| "v","v","v","^","v","^","v","^","^"
| "v","^","v","^","^","^","v","^","v"
| "^","^","^","v","v","^","v","v","v" |];
array [1..9, 1..9] of var 1..9: x;
% Standard Sudoku constraints.
constraint forall (i in 1..9) (alldifferent([x[i,j] | j in 1..9]));
constraint forall (i in 1..9) (alldifferent([x[j,i] | j in 1..9]));
constraint forall (i,j in 1..3)
( alldifferent(p,q in 1..3)( x[3*(i-1)+p, 3*(j-1)+q] ));
% Horizontal comparisons.
constraint forall (row in 1..9, c in 0..2)
( h(x[row,3*c+1], x[row,3*c+2], horizontal[row,2*c+1])
/\ h(x[row,3*c+2], x[row,3*c+3], horizontal[row,2*c+2]) ) ;
% Vertical comparisons.
constraint forall (col in 1..9, r in 0..2)
( v(x[3*r+1,col], x[3*r+2,col], vertical[2*r+1,col])
/\ v(x[3*r+2,col], x[3*r+3,col], vertical[2*r+2,col]) ) ;
% Convert a "<" or ">" string into a constraint.
predicate h(var int : a, var int : b, string : op) =
if op = "<" then a < b
elseif op = ">" then a > b
else abort("invalid horizontal operator")
endif;
% Convert a "v" or "^" string into a constraint.
predicate v(var int : a, var int : b, string : op) =
if op = "v" then a > b
elseif op = "^" then a < b
else abort("invalid vertical operator")
endif;
solve satisfy;
output [ " " ++ show(x[i,j]) ++ (if j = 9 then "\n" else "" endif)
| i,j in 1..9];
Because MiniZinc doesn’t support ragged arrays like ECLiPSe and Picat, I had to separate the horizontal and vertical clues.
Using Gecode as the solver, we get the nice result that it finds the unique solution without having to do any search.
$ mzn-gecode -s -n 0 gts.mzn
8 3 4 9 6 7 2 5 1
9 1 5 2 3 8 7 6 4
2 7 6 4 5 1 8 3 9
6 5 7 3 2 9 1 4 8
4 8 9 1 7 5 6 2 3
3 2 1 8 4 6 5 9 7
7 4 3 5 8 2 9 1 6
1 6 2 7 9 3 4 8 5
5 9 8 6 1 4 3 7 2
----------
==========
%% runtime: 0.001 (1.731 ms)
%% solvetime: 0.000 (0.332 ms)
%% solutions: 1
%% variables: 81
%% propagators: 0
%% propagations: 776
%% nodes: 1
%% failures: 0
%% restarts: 0
%% peak depth: 0