列表不等式約束

Question

我正在嘗試編寫一個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). 

Answer 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) contrains變量AnyDiff可以傳遞到貼標謂詞連同您的其他變量。通過說明AnyDiff #= 0，您可以將List1和List2限制爲相等，而AnyDiff #= 1將導致它們不相等。

Answer 2

我認爲，至少在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 ; 
... 

Answer 3

下面是基於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-predicatemaplist/4我們甚至都不需要編寫遞歸代碼！