prolog - 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 那样强烈地传播，这无疑是 SWI 的一个缺点。

然而，这里还有其他因素在起作用。

核心问题

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

| ?- X #= X。

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

(#=)/2仅适用于整数

X #= X不约束整数 X 的域以任何方式。

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

X = _#0(0..268435455)

所以，其实整数的域 X即使我们没有以任何方式限制它，它也变得有限!

为了比较，我们在 SICStus Prolog 中得到例如:

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

这说明整数 X的域没有以任何方式受到限制。

用 CLP(Z) 复制结果

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

?- 问题(A, B),
上#= 2^64，
[A,B] ins 0..Upper.

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

A = 336,
乙 = 16,
上限 = 18446744073709551616。

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

这样做的原因

中电(Z)的志向是彻底 替换低级算术谓词 在用户程序中 通过高级声明性替代方案 这可以用作真正的关系，当然也可以用作替代品。出于这个原因，CLP(Z) 支持无界整数，它可以增长到您的计算机内存允许的大小。在 CLP(Z) 中，所有整数变量的默认域是所有整数的集合。这意味着只要域之一是无限的，就不会执行应用于有界域的某些传播。

例如:

?- X #> Y，Y #> X。
X#= Y#=
这是一个有条件的答案:如果所谓的残差约束是可满足的，则原始查询是可满足的。

相反，我们得到有限域:

?- X #> Y, Y #> X, [X,Y] ins -5000..2000。
错误的。

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

固有限制

求解整数方程是 undecidable一般来说。因此，对于 CLP(Z)，我们知道没有任何决策算法总能产生正确的结果。

出于这个原因，您有时会得到残差约束而不是无条件的答案。在有限的整数集上，方程当然是可判定的:如果所有域都是有限的，并且您没有得到具体的解决方案作为答案，请使用枚举谓词之一详尽地搜索解决方案。

在可以对无限整数集进行推理的系统中，您迟早会并且必然会遇到此类现象。