clpfd 中具体化的剩余约束

Question

我定义了具体化的变体 clpfd 约束

(#<)/2

、

(#=<)/2

、

(#>=)/2

和

(#>)/2

：

:- use_module(library(clpfd)).

ltA(X,Y,Truth)  :- X #<  Y #<==> B, bool01_truth(B,Truth).
ltB(X,Y, true)  :- X #<  Y.
ltB(X,Y,false)  :- X #>= Y.

lteA(X,Y,Truth) :- X #=< Y #<==> B, bool01_truth(B,Truth).
lteB(X,Y, true) :- X #=< Y.
lteB(X,Y,false) :- X #>  Y.

gteA(X,Y,Truth) :- X #>= Y #<==> B, bool01_truth(B,Truth).
gteB(X,Y, true) :- X #>= Y.
gteB(X,Y,false) :- X #<  Y.

gtA(X,Y,Truth)  :- X #>  Y #<==> B, bool01_truth(B,Truth).
gtB(X,Y, true)  :- X #>  Y.
gtB(X,Y,false)  :- X #=< Y.

当然，

ltA/3

和

ltB/3

逻辑上等价，

lteA/3

和

lteB/3

，

gteA/3

和

gteB/3

，以及

gtA/3

和

gtB/3

。

然而，我使用这些谓词得到的答案在大小和可读性方面有所不同。我使用 SWI-Prolog 7.1.37 运行了以下查询：

首先有好消息！

?- lteA(X,Y,Truth).
Truth = false, Y#=<X+ -1 ;
Truth = true,  Y#>=X.
?- lteB(X,Y,Truth).
Truth = true,  Y#>=X ;
Truth = false, Y#=<X+ -1.

?- gteA(X,Y,Truth).
Truth = false, X#=<Y+ -1 ;
Truth = true,  X#>=Y.
?- gteB(X,Y,Truth).
Truth = true,  X#>=Y ;
Truth = false, X#=<Y+ -1.

好的！但是另外两个呢？

?- ltA(X,Y,Truth).
Truth = false, X+1#=_G968, Y#=<_G968+ -1 ;
Truth = true,  X+1#=_G912, Y#>=_G912.
?- ltB(X,Y,Truth).
Truth = true,  X#=<Y+ -1 ;
Truth = false, X#>=Y.

?- gtA(X,Y,Truth).
Truth = false, X#=<_G1301+ -1, Y+1#=_G1301 ;
Truth = true,  X#>=_G1243,     Y+1#=_G1243.
?- gtB(X,Y,Truth).
Truth = true,  Y#=<X+ -1 ;
Truth = false, Y#>=X.

不完全是！

如何使用

ltA/3

和

gtA/3

获得简洁的答案——就像使用

lteA/3

和

gteA/3

一样？

Answer 1

这与 CLP(FD) 具有紧凑性的基本思想背道而驰 答案。由于 CLP(FD) 通常不进行高斯消除， 类似的事情。它不像计算机代数系统（CAS）。

在 CLP(FD) 中，您基本上通过输入来建模您的问题 不等式，并且系统被允许对此不做任何事情 只要你不调用 labeling，就会出现不等式。

一些 CLP(FD) 实现已经检查了某些内容的一致性 输入不等式和/或已经进行简化时的程度 和繁殖。但这不是强制性的。

在您的示例中，您有 E #= X，其中 E 是一个表达式， X 是一个变量。不保证一定会发生 输入模型时 X 的值被 E 替换。

通常在 CLP(FD) 中不会这样做，因为它会爆炸 上输入的模型。你可以直接测试一下这个 没有简化：

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.4)
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam
?- use_module(library(clpfd)).
true.
?- A#=X+1, Y#=<A+ -1.
Y#=<A+ -1,
X+1#=A.

同样的情况也发生在 Jekejeke Prolog 中。 CLP(FD) 的 Jekejeke Prolog 是开源的。细化本身 已计划但尚未实施：

Jekejeke Prolog, Runtime Library 1.0.7
(c) 1985-2015, XLOG Technologies GmbH, Switzerland
?- use_module(library(finite/clpfd)).
% 11 consults and 0 unloads in 513 ms.
Yes
?- A#=X+1, Y#=<A+ -1.
A #= 1+X,
-1+A #>= Y

典型的方程 E #= X 仅在以下情况下才会导致替换： E也是变量或常数。这可能可以解释为什么你的 示例看起来因情况而异。

这里你看到SWI-Prolog简化了A#=X。我刚刚修改过 上面的例子稍微让E是一个变量：

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

在这里你可以看到 Jekejeke Prolog 正在这样做（Todo 错误修复：我 我想我需要稍微重新排序一下规则，这样就可以了 给出 A = X 而不是这里的 X = A）：

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

E #= X 的情况，其中 E 是常数，其中 传播值称为前向检查。这是 CLP(FD) 必须能够满足的最低要求，否则 标签不起作用。

但已经是 E #= X 的情况，其中 E 是变量 a 传播不是强制性的。但上面的测试表明 许多 CLP(FD) 都这样做。传播变量导致 联合查找算法等。