SWI-Prolog和约束,库CLP(FD)

Question

我正在使用clpfd库在(swi)prolog中使用约束.

我试图确定一组约束何时封装或包含另一组约束,例如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.

显然,我无法将后者传递给(Co1#/ \#\ Co2),但前者并没有给我我想要的结果.任何人都可以解释为什么这两种方法产生不同的结果,以及我如何让前者像后者一样行事？

Answer 1

您似乎正在与 CLP(FD) 打交道。这些求解器区分求解约束问题的设置阶段和标记阶段。

CLP(FD) 求解器并不能完全减少设置阶段的问题。因为它有机会在标记阶段减少变量范围。因此，在设置过程中可能会出现问题，其他求解器可以将其简化为“否”，但使用 CLP(FD) 求解器则不会。仅在标记期间才会检测到“否”。

在设置阶段减少多少很大程度上取决于给定的 CLP(FD) 系统。一些 CLP(FD) 系统在设置阶段进行更多的还原，而其他系统则做得较少。例如，GNU Prolog 使用一些索引传播，而 SWI Prolog 则没有。所以我们找到了例子，而不是你的例子：

SWI-Prolog：

?- 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-Prolog：

?- 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-Prolog：

?- 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.

再见