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

这是一个很好的观察。

乍一看，它无疑无法像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..2 ⁶⁴来使用SWI-Prolog模拟上述情况：

？-问题（A，B），
    上＃= 2 ^ 64，
   [A，B] ins 0..Upper。

作为回应，我们现在得到了SWI-Prolog：

A = 336，
B = 16
上限= 18446744073709551616。

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

的原因

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。
假。

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

固有的局限性

通常无法确定整数上的方程式。因此，对于CLP（Z），我们知道没有决策算法总是可以产生正确的结果。

因此，有时会得到剩余约束而不是无条件的答案。对于有限的整数集，方程式当然是可确定的：如果所有域都是有限的，并且您没有得到具体的解决方案作为答案，请使用枚举谓词之一详尽地搜索解决方案。

在可以推理无穷整数集的系统中，您迟早会遇到这种现象，而且必然会遇到这种现象。