prolog - 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.

start(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.

答案是有条件的:

Yes, there are solutions for X and Y provided all these conditions hold.

要获得实际值，您必须消除所有这些条件。您有多种选择:

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

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

所以只有一个解决方案。仅靠 clpfd 求解器不足以得出此结论，它需要一些额外的帮助。

更好的是使用contracting/1:

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

与标签相反，承包试图在没有(可见)搜索的情况下减小域的大小。这使得求解器变得更强大。

求解器不够强大的原因

• 在非常一般的情况下，解决此类算术问题是 undecidable .

• 在更具体的情况下，算法的成本将极其高昂。其实不止一个diophant在房间里。

• 即使是更简单的算法，在实现工作量和运行时间方面也是非常昂贵的。

• 对于许多情况，求解器归结为在一个约束内保持一致性¹。因此，不同约束之间“通信”的唯一方法是变量域。

在你的例子中，abs约束允许更多的解决方案!

?- [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).
     
| ?- 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}.
| ?- X in 1..3, Y in 1..3, abs(X-Y)#>=2, X#>Y.
     X = 3, Y = 1.

请注意abs是如何解析的!

并将 SICStus 与 library(clpz) 一起使用具有相同的强度:

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

<小时/>

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