如何在prolog中追踪clpfd的回溯？

Question

我正在用prolog和clpfd library做一个sudoku求解器。我必须跟踪回溯和每个用行和列标记的方块，以及它以以下形式获得的数字：

(1 ,1 ,1)              
(9 ,2 ,1)              
BT
(5 ,2 ,1)              

我的问题是，我如何从算法中获得上述信息？

另一个问题:算法本身是否遵守arc-consistency规则？

Answer 1

我不认为这是一个特别好的主意，但这里有一些使用SWI-Prolog的属性变量的东西，当其中一个变量被绑定时，它会打印一组变量的绑定：

:- use_module(library(clpfd)).

% Vars is a list of Name-Variable pairs where Variable is a free variable
% and Name is an atom or some other identifier for the variable.
trace_vars(Vars) :-
    maplist(trace_var(Vars), Vars).

trace_var(Vars, Id-V) :-
    when(ground(V), print_new_binding(Vars, Id-V)).

print_new_binding(Vars, Id-V) :-
    format('new binding ~w, all bindings now: ~w~n', [Id-V, Vars]).

在某种意义上，您可以使用它来“跟踪”事物：

?- Vars = [a-A,b-B,c-C], trace_vars(Vars), [A,B,C] ins 0..1, A #< B, B #< C.
new binding a-0, all bindings now: [a-0,b-_G211,c-_G217]
new binding b-1, all bindings now: [a-0,b-1,c-_G217]
false.

这只打印新的绑定，包括以前绑定的变量，但不会打印变量在回溯时变为未绑定的时刻。这些信息是隐含的(需要丑陋的黑客才能变得明确)：

?- Vars = [a-A,b-B,c-C], trace_vars(Vars), [A,B,C] ins 0..1, labeling([], [A,B,C]).
new binding a-0, all bindings now: [a-0,b-_G208,c-_G214]
new binding b-0, all bindings now: [a-0,b-0,c-_G214]
new binding c-0, all bindings now: [a-0,b-0,c-0]
Vars = [a-0, b-0, c-0],
A = B, B = C, C = 0 ;
new binding c-1, all bindings now: [a-0,b-0,c-1]
Vars = [a-0, b-0, c-1],
A = B, B = 0,
C = 1 ;
new binding b-1, all bindings now: [a-0,b-1,c-_G214]
new binding c-0, all bindings now: [a-0,b-1,c-0]
Vars = [a-0, b-1, c-0],
A = C, C = 0,
B = 1 ;
new binding c-1, all bindings now: [a-0,b-1,c-1]
Vars = [a-0, b-1, c-1],
A = 0,
B = C, C = 1 ;
new binding a-1, all bindings now: [a-1,b-_G208,c-_G214]
...

对于您的用例，请使用坐标作为Vars列表中的标识符，例如[(1,1)-Var11, (1,2)-Var12, ...]。

不过，我不认为以这种方式观察clpfd会对您有所启发。

编辑：正如mat在注释中指出的那样，向print_new_binding/2添加失败的第二个子句允许您在取消绑定之前重新访问变量：

print_new_binding(_Vars, Id-_V) :-
    format('undo binding for ~w~n', [Id]),
    false.