我正在使用 clpfd 库处理（swi）序言中的约束。
我试图确定一组约束何时封装或包含另一组，例如 X<4 封装 X<7，因为只要前者为真，后者为真。这可以很容易地用逻辑暗示来表示。但是，我无法让 #==> 运算符给我想要的结果，所以我求助于使用 not(Co1 #/\ #\Co2) ，其中 Co1 和 Co2 是约束。这对于单个约束很好，但是我想将约束的结合传递给 Co1 和 Co2。
现在问题来了。当我尝试
X#<7 #/\ #\X#<4.
我回来
X in 4..6,
X+1#=_G822,
X+1#=_G834,
_G822 in 5..7,
_G834 in 5..7.
（奇怪的是，在 Sicstus 中这样做会导致分段错误）
当我通过
X#<7,X#<4
我得到了想要的
X in inf..3.
显然，我不能将后者传递给 not(Co1 #/\ #\Co2)，但前者并没有给我想要的结果。谁能解释为什么这两种方法会产生不同的结果，以及如何让前者像后者一样行事？
对整数的一般算术约束的包含通常是不可判定的，因此所有正确的求解器都有固有的限制，超过这些限制他们必须延迟他们的答案，直到知道更多。如果您知道您的域是有限的，您可以发布域，然后尝试使用约束求解器的 labeling/2 谓词找到使暗示无效的反例。还要考虑 Q 上的线性不等式是可判定的，并且 SWI-Prolog 的库（clpq）对它们来说是完整的。因此，您可以在 CLP(Q) 中尝试您的约束：
?- use_module(library(clpq)).
true.
?- { X < 4, X >= 7 }.
false.
并且看到在 Q 中不存在这样的反例（因此在 Z 中也不存在），因此含义成立。
看来您正在处理 CLP(FD)。这些求解器区分求解约束问题的设置阶段和标记阶段。
CLP(FD) 求解器不会在设置阶段完全减少问题。因为它有机会在标记阶段减少变量范围。因此，在设置过程中可能会提出一个问题，该问题可以被其他求解器减少为“否”，但不会使用 CLP(FD) 求解器。只有在标记过程中才会检测到“否”。
在设置阶段减少多少很大程度上取决于给定的 CLP(FD) 系统。一些 CLP(FD) 系统在设置阶段做更多的减少，而其他做更少。例如，GNU Prolog 使用一些索引传播，而 SWI Prolog 则没有。因此，我们发现例如，而不是您的示例：
SWI-序言：
?- X #< Y, Y #< Z, Z #< X.
Z#=<X+ -1,
X#=<Y+ -1,
Y#=<Z+ -1.
GNU 序言：
?- X #< Y, Y #< Z, Z #< X.
(7842 ms) no
此外，由于您使用的是具体化约束，因此它还取决于具体化的完成程度。但我想在目前的情况下它只是传播问题。我们现在为您的示例找到：
SWI-序言：
?- X #< 4 #==> X #< 7.
X+1#=_G1330,
X+1#=_G1342,
7#>=_G1330#<==>_G1354,
_G1354 in 0..1,
_G1377#==>_G1354,
_G1377 in 0..1,
4#>=_G1342#<==>_G1377.
GNU 序言：
?- X #< 4 #==> X #< 7.
X = _#22(0..268435455)
在设置阶段减少更多工作和将更多工作留给标记阶段之间存在权衡。整个事情也取决于给定的例子。但是当您在设置旁边也有标签时，您不会看到结果有任何差异：
SWI-序言：
?- X in 0..9, X #< 4 #==> X #< 7, label([X]).
X = 0 ;
X = 1 ;
X = 2 ;
X = 3 ;
X = 4 ;
X = 5 ;
X = 6 ;
X = 7 ;
X = 8 ;
X = 9.
GNU 序言：
?- fd_domain(X,0,9), X #< 4 #==> X #< 7, fd_labeling([X]).
X = 0 ? ;
X = 1 ? ;
X = 2 ? ;
X = 3 ? ;
X = 4 ? ;
X = 5 ? ;
X = 6 ? ;
X = 7 ? ;
X = 8 ? ;
X = 9
我没有使用 SICStus Prolog 或 B-Prolog 进行测试。但我猜他们会在 SWI-Prolog 和 GNU Prolog 附近的某个地方表现出来。
如果您的域确实是 FD，则 CLP(Q) 不是真正的选择，因为它会错过一些“否”减少，而 CLP(FD) 不会错过。例如，以下在 CLP(FD) 中是不可满足的，但在 CLP(Q) 中是可满足的：
X = Y + 1, Y < Z, Z < X.
再见