停止 Prolog 推断值

Question

如果我运行 solved([[x, o, o], [o, o, o], [o, o, o]]) 它应该输出 true 因为只有 x 并且如果我运行 solved([[x, o, o], [o, o, o], [o, o, x]]) 它应该输出 false 因为有超过 1 x。但是，运行它在推断 C 的值时始终输出 true。

:- use_module(library(clpfd)).

rotate_clock(Xss, Zss) :-
   transpose(Xss, Yss),
   maplist(reverse, Yss, Zss).

rotate_anti(Xss, Zss) :-
   maplist(reverse, Xss, Yss),
   transpose(Yss, Zss).

linjmp([x, x, o | T], [o, o, x | T]).
linjmp([o, x, x | T], [x, o, o | T]).
linjmp([H|T1], [H|T2]) :- linjmp(T1,T2).

horizjmp([A|T],[B|T]) :- linjmp(A,B).
horizjmp([H|T1],[H|T2]) :- horizjmp(T1,T2).

jump(B,A) :- horizjmp(B,A).
jump(B,A) :- rotate_clock(B,BR), horizjmp(BR,BRJ), rotate_anti(BRJ, A).

num_x(A, C) :- count(A, x, C).

count([],X,0).
count([X|T],X,Y):- count(T,X,Z), Y is 1+Z.
count([_|T],X,Z):- count(T,X,Z).

sum_list([], 0).
sum_list([H|T], Sum) :-
   sum_list(T, Rest),
   Sum is H + Rest.

solved(A) :-
   maplist(num_x, A, B),
   sum_list(B, C),
   C == 1.

Answer 1

与其试图改变一种语言的行为（这可能是可能的，但当然是一个挑战），不如研究一下为什么最终 Prolog 会找到 C 和 C == 1.如果我们自己评估 maplist(num_x, A, B)，我们会看到：

?- maplist(num_x, [[x, o, o], [o, o, o], [o, o, x]], B).
B = [1, 0, 1] ;
B = [1, 0, 0] ;
B = [0, 0, 1] ;
B = [0, 0, 0].

因此看来 num_x/2 谓词可以生成多个结果，对于同一个列表：对于具有一个 x 的列表，它首先生成 1，然后 0.

如果我们用 count/3 做一些测试就可以确认这一点：

?- count([x, o, o], x, C).
C = 1 ;
C = 0.

?- count([x, x, o], x, C).
C = 2 ;
C = 1 ;
C = 1 ;
C = 0.

所以看起来 count/3 每次都有一个回溯点，它可以决定是否计算给定的 x。

确实，如果我们看一下 count/3 谓词，我们会看到：

count([],X,0).
count([X|T],X,Y):- count(T,X,Z), Y is 1+Z.
count(<b>[_|T]</b>,X,Z):- count(T,X,Z).

所以这里对于非空列表，有两种方式子句：一种是头部等于X，我们要统计的元素，在这种情况下是Y is 1+Z，但是最后一个子句表示，无论 head 的值是多少，Prolog 都不会计算该元素。 Prolog 执行回溯，因此最终会选择这两个子句。

我们可以添加一个dif/2来添加一个约束，即head和X应该是differrent，比如：

count([],X,0).
count([X|T],X,Y):- count(T,X,Z), Y is 1+Z.
count(<b>[H|T]</b>,X,Z):- <b>dif(H, X)</b>, count(T,X,Z).

所以现在如果 X 出现在列表中，我们将计算该元素。

停止 Prolog 推断值

Stop Prolog from inferring values

prolog

clpfd