Monotonic Knight’s Tour (CLP(Z), Scryer)

Following an exchange in #scryer on IRC, I got nerd-sniped by this prolog problem:

214520 whereiseveryone triska: in order to make knight tour logically pure, findall/3 on this line would have to be removed?                                                          
214522 whereiseveryone https://github.com/triska/clpz/blob/0c8b93accb6cfb30168228cc7e62c03beabe1d78/knight_tour.pl#L20                                                                
214540 whereiseveryone 🦆                                                                                                                                                             
215405          triska whereiseveryone: yes of course, findall/3 is not monotonic. This is a good example for a construct we need and have not yet found, notably list comprehensions.

This page documents me spending a night solving this!

Example run (monotonic)

待 scryer-prolog -f knights_tour_monotonic.pl \
  -g "assertz(clpz:monotonic), n_tour(6, Ts), append(Ts, Vs), labeling([ff], Vs), print_tour(Ts), halt"
  1  6 11 30 27  4
 10 31  2  5 12 29
  7 36  9 28  3 26
 32 23 34 19 16 13
 35  8 21 14 25 18
 22 33 24 17 20 15

This is a monotonic/pure rewrite of the classic knight_tour.pl CLP(Z) example. The only semantic change is the removal of findall/3. Successor generation is expressed as a reified list-comprehension over a finite domain, so the relation remains monotonic under clpz:monotonic.

Key points:

Core change (successors)

The non-monotonic findall/3 is replaced by an explicit domain filter. We also avoid scanning all N^2 squares by enumerating the 8 knight deltas and reifying the bounds.

successors([V|Vs], N, K0) :-
    next_candidates(N, K0, [Next|Nexts]),
    foldl(num_to_dom, Nexts, Next, Dom),
    V in Dom,
    #K1 #= #K0 + 1,
    successors(Vs, N, K1).

next_candidates(N, K0, Nexts) :-
    n_x_y_k(N, X0, Y0, K0),
    moves(Moves),
    candidate_pairs(N, X0, Y0, Moves, Pairs),
    list_comp(Pairs, pair_true_t, GoodPairs),
    pairs_keys(GoodPairs, Nexts).

List-comprehension (pure, monotonic)

The core pattern is reified filtering over a finite list. The local definition matches the library(reif) style and is kept inline for compatibility with current binaries; with the patches below, it can be dropped in favor of list_comp/3 from clpz.

list_comp([], _, []).
list_comp([E|Es], Test_2, List) :-
    if_(call(Test_2, E), List = [E|Rest], List = Rest),
    list_comp(Es, Test_2, Rest).

if_(If_1, Then_0, Else_0) :-
    call(If_1, T),
    (  T == true  -> call(Then_0)
    ;  T == false -> call(Else_0)
    ;  nonvar(T)  -> throw(error(type_error(boolean, T), _))
    ;  throw(error(instantiation_error, _))
    ).

Compact variant (patched CLPZ)

A compact variant that relies on the patched clpz exports is included as knights_tour_monotonic_clpz.pl.

Example usage (patched reif + clpz in scope):

scryer-prolog -f src/lib/reif.pl src/lib/clpz.pl knights_tour_monotonic_clpz.pl \
  -g "assertz(clpz:monotonic), n_tour(6, Ts), append(Ts, Vs), labeling([ff], Vs), print_tour(Ts), halt"

Patch diffs (apply with git apply)

Download patch: scryer-clpz-list-comp.patch

Apply from the Scryer repo root:

git apply scryer-clpz-list-comp.patch

Full diffs (for review):

src/lib/reif.pl

diff --git a/src/lib/reif.pl b/src/lib/reif.pl
index 55618e84..a38ec5f5 100644
--- a/src/lib/reif.pl
+++ b/src/lib/reif.pl
@@ -12,10 +12,11 @@ Example:
 */
 
 :- module(reif, [if_/3, (=)/3, (',')/3, (;)/3, cond_t/3, dif/3,
-                memberd_t/3, tfilter/3, tmember/2, tmember_t/3,
-                tpartition/4]).
+                memberd_t/3, tfilter/3, list_comp/3, list_comp/4,
+                tmember/2, tmember_t/3, tpartition/4]).
 
 :- use_module(library(dif)).
+:- use_module(library(lists), [maplist/3]).
 
 :- meta_predicate(if_(1, 0, 0)).
 
@@ -42,12 +43,21 @@ non(true, false).
 non(false, true).
 
 :- meta_predicate(tfilter(2, ?, ?)).
+:- meta_predicate(list_comp(?, 2, ?)).
+:- meta_predicate(list_comp(?, 2, 2, ?)).
 
 tfilter(_, [], []).
 tfilter(C_2, [E|Es], Fs0) :-
    if_(call(C_2, E), Fs0 = [E|Fs], Fs0 = Fs),
    tfilter(C_2, Es, Fs).
 
+list_comp(Domain, Test_2, List) :-
+   tfilter(Test_2, Domain, List).
+
+list_comp(Domain, Test_2, Map_2, List) :-
+   tfilter(Test_2, Domain, Filtered),
+   maplist(Map_2, Filtered, List).
+
 :- meta_predicate(tpartition(2, ?, ?, ?)).
 
 tpartition(P_2, Xs, Ts, Fs) :-

src/lib/clpz.pl

diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl
index 35b16aa8..035f5e46 100644
--- a/src/lib/clpz.pl
+++ b/src/lib/clpz.pl
@@ -101,6 +101,11 @@
                  fd_size/2,
                  fd_dom/2,
 
+                 % reification helpers
+                 if_/3,
+                 list_comp/3,
+                 list_comp/4,
+
                  % for use in predicates from library(reif)
                  clpz_t/2,
                  (#=)/3,
@@ -126,6 +131,7 @@
 :- use_module(library(arithmetic)).
 :- use_module(library(debug)).
 :- use_module(library(format)).
+:- use_module(library(reif), []).
 
 % :- use_module(library(types)).
 
@@ -196,6 +202,23 @@ domain_error(Expectation, Term) :-
 type_error(Expectation, Term) :-
         type_error(Expectation, Term, unknown(Term)-1).
 
+/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+  Reification helpers (from library(reif)).
+- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
+
+:- meta_predicate(if_(1, 0, 0)).
+:- meta_predicate(list_comp(?, 2, ?)).
+:- meta_predicate(list_comp(?, 2, 2, ?)).
+
+if_(If_1, Then_0, Else_0) :-
+        reif:if_(If_1, Then_0, Else_0).
+
+list_comp(Domain, Test_2, List) :-
+        reif:list_comp(Domain, Test_2, List).
+
+list_comp(Domain, Test_2, Map_2, List) :-
+        reif:list_comp(Domain, Test_2, Map_2, List).
+
 
 :- meta_predicate(partition(1, ?, ?, ?)).

Files