For better or worse, Youtube videos trigger my ADHD like nothing else. But apparently I sat through 25 minutes of some guy solving a sudoku. I even hate sudoku. It's mechanical and tedious, and that might even be part of the point (no slight intended to anyone who like sudoku btw).

The video was not just interesting because of the unbridled excitement of the solver which we got to see vicariously, or the nicely patterned unique answer in the end, but because I didn't know the community ventures into interesting modification of base rules like that. On some reading, none of the Anti-Knight, Anti-King or Non-Consecutive rule seem to be novel, though perhaps their combination is.

Now, in the way people are partial to movies or shows they watched when they were younger, sudoku always reminds me of Peter Norvig's sudoku page. Rose tinted glass or not, I remember it as one of the most beautiful/idiomatic snippet of code I had ever seen. I remember porting it to some different language, and being blown away by the fact that for many problems of the newspaper variety, just the constraint propagation alone is sufficient without even employing search. Even though in the video the solver didn't branch and backtrack, some of his reasoning seemed more advanced than basic constraint propagation. How would a computer fare here, then?

This is a good opportunity to try out a system I admire from sideline, it's called Picat. It's pretty much a Prolog engine with enough syntactic sugar to be a decent general purpose language. Now, an argument could be made that such a thing is better realised as an embedded DSL as part of a nicer host language. The benefit is that it can integrate with rest of the system much better, and you get all the toolings for free. See for example, Core.Logic (Clojure), Screamer (CL) or any of the Kanrens, or Picolisp or Shen. It's no surprise that the list goes on for Lisps, because DSL is bread and butter for them. This isn't to say logic programming can't also be offered through a library, the distinction can be blurry anyway. But Picat is not just like the DSLs I have mentioned. It provides a uniform frontend API for many different flavours of solvers in the backend, so in that regard it's more akin to MiniZinc, or the analogous library is google's or-tools perhaps.

Digression aside, sudoku is pretty much modeling language 101. The encoding for basic sudoku rules can be done as simply as:

import smt, util.

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

  % Row Constraint
  foreach(Row in Board) all_different(Row) end,

  % Column Constraint
  foreach(Col in transpose(Board)) all_different(Col) end,

  % Sub-grid Constraint
  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,
  
  solve(Board).

board(Board) =>
  Board = {
    {8,_,_, _,_,_, _,_,_},
    {_,_,3, 6,_,_, _,_,_},
    {_,7,_, _,9,_, 2,_,_},
    
    {_,5,_, _,_,7, _,_,_},
    {_,_,_, _,4,5, 7,_,_},
    {_,_,_, 1,_,_, _,3,_},
    
    {_,_,1, _,_,_, _,6,8},
    {_,_,8, 5,_,_, _,1,_},
    {_,9,_, _,_,_, 4,_,_}
  }.

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

When run:

CPU time 0.005 seconds. Backtracks: 0

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

It's self-explanatory, just as any modeling language should be. And just like that I know the answer of Arto Inkala's "hardest problem ever" in a blink. Specifying the new constraints for miracle sudoku is just a little more verbosity:

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.

And when this is run:

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}