这是一个很好的观察。
乍一看,毫无疑问,SWI 的一个缺点是它无法像 GNU Prolog 那样强大地传播。
然而,这里还有其他因素在起作用。
核心问题
首先,请在 GNU Prolog 中尝试以下查询:
| ?- X #= X。
声明式地,查询可以读作:X
is an integer。原因是:
(#=)/2
仅适用于整数
X #= X
不X
以任何方式约束整数的域。
然而,至少在我的机器上,GNU Prolog 回答:
X = _#0( 0 .. 268435455 )
所以,事实上,尽管我们没有以任何方式限制它,但整数的域X
已经变得有限!
作为比较,我们以 SICStus Prolog 为例:
?- X #= X.
X inf..sup.
这表明整数的域X
没有受到任何限制。
用 CLP(Z) 复制结果
让我们公平竞争。我们可以通过人为地将变量的域限制为有限区间 0..2 64来使用 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),我们知道不存在始终产生正确结果的决策算法。
出于这个原因,您有时会得到剩余约束而不是无条件的答案。在有限的整数集合上,方程当然是可判定的:如果所有域都是有限的并且您没有得到具体的解决方案作为答案,请使用枚举谓词之一来穷举搜索解决方案。
在可以推理无限整数集的系统中,您迟早会遇到这样的现象。