我正在尝试编写一个prolog(clp)谓词,该谓词将构建两个列表的约束不等式。
更正式地,有两个列表A=[A1,...,AN], B=[B1,...,BN]
约束定义为(A1 #= B1) #/ (A2 #= B2) #/ ... #/ (AN #= BN)
。
我不确定如何在给定两个任意长度列表给定两个列表中构建此约束。这是我的尝试。我知道为什么它不起作用,但不能修复它。
any_different([], []).
any_different([H1|T1], [H2|T2]):-
H1 #= H2 #/ any_different(T1, T2).
您需要建立分离并通过第三个参数将其返回:
any_different([], [], V) :-
V #= 0. % no differences between [] and []
any_different([H1|T1], [H2|T2], Disj) :-
any_different(T1, T2, Disj0),
Disj #<==> (H1 #= H2) #/ Disj0.
现在,调用any_different(List1, List2, AnyDiff)
违反了一个可变AnyDiff
,您可以将其与其他变量一起传递给标签谓词。通过说明AnyDiff #= 0
,您可以将List1
和List2
限制为相等,而AnyDiff #= 1
将导致它们不平等。
我认为,至少在swi-prolog中,谓词dif/2和库(clpfd)可以替代重新化:
?- L=[X,Y,Z], L ins 1..3, dif(L,[1,2,3]), label(L).
L = [1, 1, 1],
X = Y, Y = Z, Z = 1 ;
L = [1, 1, 2],
X = Y, Y = 1,
Z = 2 ;
...
这是基于sum/3
和CLPFD重新化(#<==>)/2
的实现:
not_equals_reified(X, Y, B) :-
X #= Y #<==> B.
any_different(Xs, Ys) :-
maplist(not_equals_reified, Xs, Ys, Bs),
sum(Bs, #>, 0).
通过使用meta-Prodicate maplist/4
,我们甚至不需要编写递归代码!