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

Christopher Mears, 6 January 2015