列表不等式约束答案

【问题标题】：List inequality constraint列表不等式约束
【发布时间】：2015-12-11 00:13:26
【问题描述】：

我正在尝试编写一个 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).

【问题讨论】：

标签： prolog clpfd

【解决方案1】：

您需要构建析取并通过第三个参数返回它：

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 将导致它们不相等。

【讨论】：

谢谢。这是我一直在寻找的成语。

【解决方案2】：

我认为，至少在 SWI-Prolog 中，谓词 dif/2 和 library(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 ;
...

【讨论】：

【解决方案3】：

这是一个基于 sum/3 和 clpfd reification (#<==>)/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-predicate maplist/4，我们甚至不需要编写递归代码！

【讨论】：