SWI Prolog与GNU Prolog - SWI下的CLP（FD）问题

Question

我在Prolog中写了一个快速谓词，尝试了CLP（FD）及其解决方程组的能力。

problem(A, B) :-
    A-B #= 320,
    A #= 21*B.

当我在SWI中调用它时，我得到：

?- problem(A,B).
320+B#=A,
21*B#=A.

在GNU中，我得到了正确答案：

| ?- problem(A,B).

A = 336
B = 16

这里发生了什么？理想情况下，我希望在SWI中获得正确的结果，因为它是一个更加强大的环境。

Answer 1

这是一个很好的观察。

乍一看，毫无疑问，它似乎是SWI的一个缺点，它无法像GNU Prolog那样强大地传播。

但是，这里还有其他因素在起作用。

The core issue

首先，请在GNU Prolog中尝试以下查询：

| ?- X #= X.

声明性地，查询可以读作：X是一个整数。原因是：

• (#=)/2仅适用于整数
• X #= X不以任何方式约束整数X的域。

但是，至少在我的机器上，GNU Prolog回答：

X = _#0(0..268435455)

所以，实际上，整数X的域已经变得有限，即使我们没有以任何方式限制它！

为了比较，我们在SICStus Prolog中得到了例子：

?- X #= X.
X in inf..sup.

这表明整数X的域没有受到任何限制。

Replicating the result with CLP(Z)

让我们平衡竞争环境。我们可以通过人为地将变量的域限制为有限区间0..264来模拟SWI-Prolog的上述情况：

?- problem(A, B),
   Upper #= 2^64,
   [A,B] ins 0..Upper.

作为回应，我们现在使用SWI-Prolog：

A = 336,
B = 16,
Upper = 18446744073709551616.

因此，将域限制为有限的整数子集使我们能够使用SWI-Prolog的CLP（FD）求解器或其后继者CLP(Z)复制我们从GNU Prolog中获知的结果。

The reason for this

CLP（Z）的目标是通过高级声明性替代方案完全取代用户程序中的低级算术谓词，这些替代方案可以用作真正的关系，当然也可以作为替代品。因此，CLP（Z）支持无界整数，它可以增长到计算机内存允许的大小。在CLP（Z）中，所有整数变量的默认域是所有整数的集合。这意味着只要其中一个域是无限的，就不会执行应用于有界域的某些传播。

例如：

?- X #> Y, Y #> X.
X#=<Y+ -1,
Y#=<X+ -1.

这是一个条件答案：如果所谓的残差约束是可满足的，则原始查询是可满足的。

相反，我们得到有限域：

?- X #> Y, Y #> X, [X,Y] ins -5000..2000.
false.

只要所有域都是有限的，我们期望所涉及的系统具有大致相同的传播强度。

An inherent limitation

求解整数方程式一般是undecidable。因此，对于CLP（Z），我们知道没有决策算法能够始终产生正确的结果。

因此，您有时会获得剩余约束而不是无条件答案。在有限的整数集上，方程式当然是可判定的：如果所有域都是有限的并且您没有得到具体的解决方案作为答案，则使用其中一个枚举谓词来穷举搜索解决方案。

在可以推理无限整数集的系统中，你迟早会遇到这样的现象。