使用约束处理规则解决 N 皇后问题

Question

我在使用 CHR 解决需要回溯的问题时遇到了明显的问题。我确信在某个地方使用 CHR 有一个经典的解决方案来解决这个问题，但我似乎找不到它。

我的代码如下所示：

:- 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).

正如人们所期望的，它生成以下不完整的解决方案：

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

有没有一种简单的方法可以让 CHR 回溯并找到正确的解决方案？

Answer 1

有没有一种简单的方法可以让 CHR 回溯并找到正确的解决方案？

CHR 的基本原则是一旦约束匹配并且守卫成功，就承诺遵守规则。

如果可以找到必要的被动约束，并且与规则头和规则守卫都匹配成功，则规则被提交并执行规则体。
-- https://www.swi-prolog.org/pldoc/man?section=chr-syntaxandsemantics

所以答案是：不，没有（直接）方法以与其设计相矛盾的方式使用功能。

Core Prolog 是您想要生成和“搜索”解决方案空间的方式，而 CHR 是您想要验证解决方案是否有效的方式。