prolog - 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) 中完成，因为它会吹up 输入的模型。你可以直接测试这个不简化:

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 中。中电( FD )的Jekejeke Prolog 是开源的 here .精化本身已计划但尚未实现:

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 是常数，而 this值被传播称为前向检查。这是CLP(FD) 必须能够满足的最低要求，否则贴标签是行不通的。

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

再见