我正在尝试用Prolog解决一个逻辑难题,作为一个学习练习,我认为我已经使用GNU Prolog有限域求解器正确地映射了这个问题。
当我运行solve函数时,Prolog返回:yes和一个在0..1范围内的变量列表(布尔值,因为我已经限制了它们)问题是,当我尝试添加fd_labeling(Solution)子句时,Prolog about faces并吐出:no.
我是这门语言的新手,我似乎找不到任何攻击过程来弄清楚为什么一切似乎都有效,直到我真正要求它标记答案…
显然,您没有"正确"地将问题映射到FD,因为当您尝试标记变量时,您会得到"否"。
您在约束逻辑编程中所做的是建立约束模型,其中您拥有具有域的变量(在您的示例中,布尔值具有域[0,1]),以及这些变量之间的许多约束。每个约束都有一个传播规则,该规则试图为发布约束的变量的域实现一致性。不一致的值将从域中删除。一致性有几种类型,但它们有一个共同点:约束本身通常不会给你一个完整的解决方案,甚至不会告诉你约束模型是否有解决方案。
举个例子,假设你有两个变量X和Y,它们的域都是[1..]10],约束X <Y.然后传播规则将值1从Y的域中移除,并从x的域中移除10。然后它将停止,因为这些域现在是一致的:对于一个域中的每个值,在另一个域中存在一个值,从而满足约束。>
为了得到一个解决方案(其中所有变量都绑定到值),您需要标记变量。每次标记都会唤醒附加到标记变量上的约束,从而触发另一轮传播。这将导致一个解决方案(所有变量绑定值,答案:是)或失败(在每个搜索树的分支中,一些变量以空域结束,答案:否)
由于每个约束只针对它所发布的变量域的一致性,因此在传播阶段可能不会检测到由约束组合引起的不可行性。例如,三个变量X,Y,Z,域为[1..][2],以及两两不等式约束。这似乎发生在你的约束模型上。
如果你确信这个谜题一定有解决方案,那么你的约束模型就包含了一些不可行性。也许仔细观察约束条件已经足以发现它了。
如果你没有看到任何明显的不可行性(例如,一些矛盾的约束,如上面的不等式例子),你需要调试你的程序。如果可能的话,不要使用内置的标记谓词,而是编写自己的谓词。然后,您可以添加一些输出谓词,允许您跟踪实例化了什么变量,以及这导致了布尔决策变量中的哪些变化,或者它是否导致了失败。
(@twinterer已经给出了解释,我的回答试图从不同的角度来解释)
当你输入一个查询到Prolog时,你得到的是一个答案。通常一个答案包含一个解决方案,有时它包含几个解决方案,有时它根本不包含任何解决方案。这两个概念经常被混淆。让我们看一下使用GNU Prolog的例子:
| ?- length(Vs,3), fd_domain_bool(Vs).
Vs = [_#0(0..1),_#19(0..1),_#38(0..1)]
yes
这里,我们有一个包含8个解的答案。即:
| ?- length(Vs,3), fd_domain_bool(Vs), fd_labeling(Vs).
Vs = [0,0,0] ? ;
Vs = [0,0,1] ? ;
...
Vs = [1,1,1]
yes
现在是另一个查询。这就是@twinterer提到的例子。
| ?- length(Vs,3), fd_domain_bool(Vs), fd_all_different(Vs).
Vs = [_#0(0..1),_#19(0..1),_#38(0..1)]
yes
答案看起来和以前一样。然而,它不再包含解决方案。
| ?- length(Vs,3), fd_domain_bool(Vs), fd_all_different(Vs), fd_labeling(Vs).
no
理想情况下,在这种情况下,高层不会说"是",而是说"可能"。事实上,CLP(R),最早的约束系统之一,就是这样做的。
另一种让它不那么神秘的方法是显示实际的约束条件。SWI这样做:
?- length(Vs,3), Vs ins 0..1, all_different(Vs).
Vs = [_G565,_G568,_G571],
_G565 in 0..1,
all_different([_G565,_G568,_G571]),
_G568 in 0..1,
_G571 in 0..1.
?- length(Vs,3), Vs ins 0..1, all_different(Vs), labeling([], Vs).
false.
SWI显示了所有需要满足的约束条件来得到一个具体的解。请阅读SWI的回答:是的,有一个解决方案,前提是所有这些小字都是真的!唉,小字是假的。
解决这个问题的另一种方法是获得具有更强一致性的all_different/1
的实现。但这只在特定情况下有效。
?- length(Vs,3), Vs ins 0..1, all_distinct(Vs).
false.
在一般情况下,你不能期望系统保持全局一致性。原因:
保持一致性是非常昂贵的。将这些决定委托给标签通常会更好。事实上,简单的
all_different/1
往往比all_distinct/1
更快。更好的一致性算法通常非常复杂。
在一般情况下,保持全局一致性是一个无法确定的问题。