swi-prolog abs运算符不在clpfd模块中工作

Question

我正在使用swi-prolog中的CLPFD库进行一些玩具测试.

有谁知道为什么下面的程序不起作用？

start(X,Y):- 
   Vars = [X,Y],
   Vars ins 1..3,
   abs(X-Y) #>= 2,
   X #>= Y,
   nl,
   write([X,Y]), nl.

开始(X,Y)的预期答案是X = 3和Y = 1.但是,swi-prolog指出了我的答案.如果我更换,该程序正常工作

abs(X-Y) #>= 2

通过

X-Y #>= 2

我的问题是我是否以正确的方式使用abs运算符.

Answer 1

首先,约束和副作用并没有聚集在一起.相反,只需坚持你的程序的纯粹部分:

start(X,Y):- 
   Vars = [X,Y],
   Vars ins 1..3,
   abs(X-Y) #>= 2,
   X #>= Y.

现在,查询你的关系:

?- start(X,Y).
X in 1..3,
X#>=Y,
abs(X-Y)#>=2,
Y in 1..3.

答案是有条件的:

是的,有解决方案,X并Y提供所有这些条件.

要获得实际值,您必须消除所有这些条件.你有几个选择:

在这种情况下,您可以使用labeling/2:

?- start(X,Y), labeling([], [X,Y]).
X = 3,
Y = 1.

所以只有一个解决方案.clpfd单独使用-solver并不足以得出这个结论,它需要一些额外的帮助.

更好的是使用contracting/1:

?- start(X,Y), clpfd:contracting([X,Y]).
X = 3,
Y = 1.

与标记相反,合同尝试在没有(可见)搜索的情况下减小域的大小.这使得求解器更强一些.

解算器不够强大的原因

• 在一般情况下解决这样的算术问题是不可判定的.

• 在更具体的情况下,算法将是非常昂贵的.事实上,房间里有不止一个桡骨病.

• 就实现工作量和运行时而言,即使是更简单的算法也是非常昂贵的.

• 在许多情况下,求解器归结为在一个约束内保持一致性¹.因此,在不同约束之间"通信"的唯一方法是变量域.

在您的情况下,abs-constraint允许更多解决方案!

?- [X,Y]ins 1..3, abs(X-Y)#>=2, labeling([],[X,Y]).
X = 1,
Y = 3 ;
X = 3,
Y = 1.

?- [X,Y]ins 1..3, X-Y#>=2, labeling([],[X,Y]).
X = 3,
Y = 1.

你期望的是额外的约束X #>= Y会有所帮助.唉,具体的一致性机制太弱了.甚至没有X #> Y帮助:

?- [X,Y]ins 1..3, abs(X-Y)#>=2, X#>Y.
X in 2..3,
Y#=<X+ -1,
abs(X-Y)#>=2,
Y in 1..2.

但是,如果从SWI切换到SICStus,情况会有所不同:

| ?- assert(clpfd:full_answer).
yes
| ?- X in 1..3, Y in 1..3, abs(X-Y)#>=2.
Y+_A#=X,
X in 1..3,
Y in 1..3,
_A in{-2}\/{2} ? ;
no
| ?- X in 1..3, Y in 1..3, abs(X-Y)#>=2, X#>Y.
X = 3,
Y = 1 ? ;
no

请注意abs是如何解决的!

使用SICStus library(clpz)具有相同的强度:

| ?- X in 1..3, Y in 1..3, abs(X-Y)#>=2, X#>Y.
X = 3,
Y = 1 ? ;
no

^{1请注意,我避免使用局部一致性的概念而不是全局一致性,因为通常全局一致性仅指一个"全局"约束内的一致性.}