Solving the “Miracle Sudoku” in Prolog

Solving the “Miracle Sudoku” in Prolog
benjamincongdon.me

A CLP(FD/ℤ) solution such as this one has two parts: First, the relevant constraints are posted. Second, a search tries to find concrete solutions. In general, a search is necessary because the constraints by themselves are not sufficient to deduce the unique solution as that would be computationally prohibitive.

You can therefore influence the speed of the logic program in two categorically distinct ways: First, you can post different constraints or try a different formulation altogether. Second, you can try different search heuristics that try to find concrete solutions more efficiently.

Regarding constraint propagation, there is a clear trade-off between strength and efficiency of propagation. For instance, the all_distinct/1 constraint that is used in the sample solution propagates very strongly, and is therefore much slower than the weaker all_different/1 constraint, even though they are completely equivalent from a semantic perspective: Both are true if and only if the given integers are pairwise distinct. It depends on the problem at hand whether the stronger propagation pays off, or whether the weaker propagation is in fact sufficient to quickly find solutions.

Especially for very simple tasks such as Sudoku, quick and weak propagation may well outperform strong and slow propagation.

In this concrete example, I easily achieved a 20-fold speedup by replacing the all_distinct/1 constraint with all_different/1, and using the ff labeling strategy to search for concrete solutions. ff means first-fail, and is often a very good strategy. To get this, I simply textually replaced all occurrences of all_distinct with all_different in the source code, and posted:

    ?- problem(1, Rows),
       sudoku(Rows),
       append(Rows, Vs),
       labeling([ff], Vs),
       maplist(portray_clause, Rows).

And this is one of the key attractions of constraint logic programming (CLP): You can relatively easily try different search strategies while keeping the model the same.

In Hakan's very nice Picat solution, you see that a specific search heuristic is used, specified as:

    solve([ffd,down], Vars).

I suspected something like the `ff` labeling approach would improve the solution, but I had no idea how much of a difference `all_different` made vs. `all_distinct`!