如何在序言中追蹤clpfd的回溯？

Question

我正在使用clpfd library與prolog解決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在工作會啓發你。

編輯：作爲墊指出的意見，增加了失敗秒子句print_new_binding/2讓您的結合破滅前重溫一個變量：

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