Solving "Miracle" Sudoku in Picat

gistfile1.txt

λ picat miracle.pi                                                       

CPU time 0.034 seconds. Backtracks: 0

{4,8,3,7,2,6,1,5,9}
{7,2,6,1,5,9,4,8,3}
{1,5,9,4,8,3,7,2,6}
{8,3,7,2,6,1,5,9,4}
{2,6,1,5,9,4,8,3,7}
{5,9,4,8,3,7,2,6,1}
{3,7,2,6,1,5,9,4,8}
{6,1,5,9,4,8,3,7,2}
{9,4,8,3,7,2,6,1,5}

miracle.pi

import smt, util.


sudoku(Board) =>
  N = Board.length,
  S = N.sqrt.ceiling,
  Board :: 1..N,

  % Normal sudoku constraints
  foreach(Row in Board) all_different(Row) end,
  foreach(Col in transpose(Board)) all_different(Col) end,
  foreach(I in 1..S..N, J in 1..S..N)
    all_different([Board[I + K, J + L] : K in 0..2, L in 0..2])
  end,
  
  % neighbours
  Ngb = [(A, B) : A in -2..2, B in -2..2, member(abs(A) + abs(B), 1..3)],
  
  foreach(I in 1..N, J in 1..N, (X, Y) in Ngb, member(I + X, 1..N), member(J + Y, 1..N))
    % knight and king constraint
    Board[I, J] #!= Board[I + X, J + Y],

    % orthogonally adjacent constraint
    if (abs(X) + abs(Y) = 1) then
      abs(Board[I, J] - Board[I + X, J + Y]) #!= 1
    end
  end,
    
  solve(Board).

board(Board) =>
  Board = {
    {_,_,_, _,_,_, _,_,_},
    {_,_,_, _,_,_, _,_,_},
    {_,_,_, _,_,_, _,_,_},
    
    {_,_,_, _,_,_, _,_,_},
    {_,_,1, _,_,_, _,_,_},
    {_,_,_, _,_,_, 2,_,_},
    
    {_,_,_, _,_,_, _,_,_},
    {_,_,_, _,_,_, _,_,_},
    {_,_,_, _,_,_, _,_,_}
  }.

main =>
  board(Board),
  time2(sudoku(Board)),
  foreach(I in Board) println(I) end.