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

首先，约束和side-effects不会聚集在一起。相反，只需坚持程序的纯粹部分：

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-solver 本身还不足以得出这个结论，它需要一些额外的帮助。

更好的方法是使用 contracting/1:

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

与标签相反，合同试图在没有（可见的）搜索的情况下减小域的大小。这使求解器更强大。

求解器不够强大的原因

在非常一般的情况下，解决此类算术问题是 undecidable。
在更具体的情况下，算法的成本会非常高。其实房间里不止一个diophant
即使是更简单的算法，在实施工作和运行时方面的成本也非常高。
对于许多情况，求解器归结为在一个约束¹ 内保持一致性。因此，在不同约束之间 "communicate" 的唯一方法是变量域。

在你的情况下，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是如何解析的！

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

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

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

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

swi-prolog abs operator not working in clpfd module

prolog

swi-prolog

clpfd