prologconstraint-handling-rules

Solving N-queens with Constraint Handling Rules


I've run into the obvious problem with using CHR to solve a problem that requires backtracking. I'm sure there is a classic solution to this problem using CHR somewhere but I can't seem to find it.

My code looks like this:

:- use_module(library(chr)).

:- chr_constraint board(+int), free(+int, +int), queen/0, queen(+int, +int). 
:- chr_constraint attacked(+int, +int), queens(+int), n_queens(+int).

%% initialize the board
board(N) <=> foreach(between(1, N, X), foreach(between(1, N, Y), free(X, Y))).

%% place a queen
queen, free(X, Y) <=> queen(X, Y).
queen(X, _) \ free(X, F) <=> attacked(X, F).
queen(_, Y) \ free(F, Y) <=> attacked(F, Y).
queen(X1, Y1) \ free(X2, Y2) <=> diagonal(X1, Y1, X2, Y2) | attacked(X2, Y2).

%% generate all the necessary queens
queens(0) <=> true.
queens(N) <=> queen, succ(N0, N), queens(N0).

%% ascertain if two points are on the same diagonal
diagonal(X1, Y1, X2, Y2) :-
    abs(X1 - X2) =:= abs(Y1 - Y2).

n_queens(N) <=> board(N), queens(N).

main :-
    n_queens(8).

As one would expect, it generates the following incomplete solution:

queen,
queen,
queen,
queen(4, 5),
queen(5, 7),
queen(6, 4),
queen(7, 6),
queen(8, 8),
...

Is there a straightforward way to enable CHR to backtrack and find the right solutions here?


Solution

  • Is there a straightforward way to enable CHR to backtrack and find the right solutions here?

    A fundamental principle of CHR is commitment to a rule once constraints are matched and a guard succeeds.

    If the necessary passive constraints can be found and all match with the head of the rule and the guard of the rule succeeds, then the rule is committed and the body of the rule executed.
    -- https://www.swi-prolog.org/pldoc/man?section=chr-syntaxandsemantics

    So the answer is: no, there is no (straightforward) way to use a feature in a way that contradicts its design.

    Most likely, core Prolog is how you want to generate and "search" your solution space, and CHR is how you want to verify that your solution is valid. But, CHR is Turing complete, so it would be wrong to claim that n-queens cannot be solved fully in CHR.