我正在使用 clpfd 库处理 (swi) prolog 中的约束。
我正在尝试确定一组约束何时封装或包含另一组约束，例如X 运算符给我想要的结果，所以我求助于使用 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)，但前者并没有给我想要的结果。谁能解释为什么这两种方法会产生不同的结果，以及如何让前者像后者一样行事？
【问题讨论】：
标签： prolog constraints clpfd clpq
对整数的一般算术约束的包含通常是不可判定的，因此所有正确的求解器都有固有的限制，超过这些限制他们必须延迟他们的答案，直到知道更多。如果您知道您的域是有限的，您可以发布域，然后尝试使用约束求解器的 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.
再见
【讨论】：