SWI-Prolog和约束，库CLP（FD） [英] SWI-Prolog and constraints, library CLP(FD)
问题描述
我使用clpfd库在（swi）prolog中约束。
我试图识别一组约束封装或包含其他，例如X <4封装X <7，只要前者为真，后者为真。这可以使用逻辑含义来容易地表示。但是，我不能得到＃==>运算符给我想要的结果，所以我诉诸使用不（Co1＃/ \＃\Co2）其中Co1和Co2是约束。这对于个体约束是很好的，但是我想将约束的连接传递给Co1和Co2。
现在这里是rub。当我尝试
X＃< 7＃/ \＃\X＃< 4。
我回来了
X in 4..6，
X + 1＃= _ G822，
X + 1＃= _ G834，
_G822 in 5..7，
_G834在5..7。
（奇怪的是，在Sicstus中执行此操作会导致细分错误）
当我通过
X＃<7，X＃<4
我得到所需的
X in inf..3。
显然，我不能将后者传递给不是（Co1＃/ \＃\Co2 ），但前者不给我我想要的结果。任何人都可以解释为什么这两种方法产生不同的结果，以及我如何让前者像后者一样行事。
似乎你在处理CLP（FD）。这些求解器区分了求解约束问题的建立阶段和标记阶段。
CLP（FD）求解器在设置阶段没有完全减少问题。因为它有机会在标记阶段减少可变范围。因此，可能在设置期间提出问题，其可以通过其他求解器被减少为否，但是它不会具有CLP（FD）求解器。只有在标记期间，才会检测到否。
在设置阶段完成的减少量高度取决于给定的CLP（FD）系统。一些CLP（FD）系统在设置阶段执行更多减少，而其他更少。例如，GNU Prolog使用一些索引传播，而SWI Prolog则没有。因此，我们找到例如，不是你的例子：
SWI-Prolog：
？ - X＃< Y，Y＃ Z， X
Z＃=< X + -1，
X＃=< Y + -1，
Y＃=< Z + -1。
GNU Prolog：
？ - X＃< Y，Y＃ Z， X.
（7842 ms）no
一点点是如何聪明的完成。但我想在目前的情况下，它只是一个传播的问题。现在我们找到您的示例：
SWI-Prolog：
α-X＃ 4＃==> X＃<
X + 1＃= _ G1330，
X + 1＃= _ G1342，
7＃> = _G1330＃== _G1354，
_G1354 in 0 ..1，
_G1377＃==> _G1354，
_G1377在0..1中，
4＃> = _G1342＃==> _G1377。
GNU Prolog：
？ - 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 Prolog：
？ - 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 + Y< Z， X.
再见
I'm playing around with constraints in (swi) prolog using the clpfd library.
I'm trying to identify when one set of constraints encapsulates or subsumes the other, e.g. X<4 encapsulates X<7 as whenever the former is true, the latter is true. This can be easily represented using logical implication. However, I couldn't get the #==> operator to give me the result I wanted, so I resorted to using not(Co1 #/\ #\Co2) where Co1 and Co2 are constraints. This is fine for individual constraints, but I then wanted to pass a conjunctions of constraints into Co1 and Co2.
Now here is the rub. When I try
X#<7 #/\ #\X#<4.
I get back
X in 4..6,
X+1#=_G822,
X+1#=_G834,
_G822 in 5..7,
_G834 in 5..7.
(oddly enough, doing this in Sicstus results in a segmentation fault)
When I pass in
X#<7,X#<4
I get the desired
X in inf..3.
Obviously, I can't pass the latter into not(Co1 #/\ #\Co2), but the former doesn't give me the result I want. Can anyone explain why the two approaches yield different results, and how I can get the former to act like the latter?
It seems you are dealing with CLP(FD). These solvers distinguish the setup phase and the labeling phase of solving a constraint problem.
A CLP(FD) solver does not completely reduce a problem during the setup phase. Since it has the chance to reduce variable ranges during the labeling phase. Thus it could be that during setup a problem is posed which could be reduced by other solvers to "No", but it will not with a CLP(FD) solver. Only during labeling a "No" will be detected.
How much reduction is done during the setup phase highly depends on the given CLP(FD) system. Some CLP(FD) systems do more reduction during the setup phase, while other do less. GNU Prolog for example uses some indexical propagation, whereas SWI Prolog does not. So we find for example, not your example:
SWI-Prolog:
?- X #< Y, Y #< Z, Z #< X.
Z#=<X+ -1,
X#=<Y+ -1,
Y#=<Z+ -1.
GNU Prolog:
?- X #< Y, Y #< Z, Z #< X.
(7842 ms) no
Further since you are using reified constraints it also depends a little bit how clever the reification is done. But I guess in the present case its only a matter of propagation. We find now for your example:
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 Prolog:
?- X #< 4 #==> X #< 7.
X = _#22(0..268435455)
There is a tradeoff between doing more reduction in the setup phase and leaving more work to the labeling phase. And the whole matter also depends on the given example. But when you have also labeling beside setup, you will not see any difference in terms of outcome:
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 Prolog:
?- 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
I didn't test with SICStus Prolog or B-Prolog. But I guess they will behave somewhere in the vincinity of SWI-Prolog and GNU Prolog.
CLP(Q) is no real alternative if your domain is really FD, since it will miss some "No" reductions, which CLP(FD) would not miss. For example the following is unsatisfiable in CLP(FD), but satisfiable in CLP(Q):
X = Y + 1, Y < Z, Z < X.
Bye
这篇关于SWI-Prolog和约束，库CLP（FD）的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
