使用 clpfd Prolog 库解决斑马谜题（又名爱因斯坦谜题）

Posted 2023-05-08

【中文标题】使用 clpfd Prolog 库解决斑马谜题（又名爱因斯坦谜题）

【英文标题】：Solving the Zebra puzzle (aka. Einstein puzzle) using the clpfd Prolog library

【发布时间】：2012-06-22 18:45:59

【问题描述】：

我得到了一个使用我选择的约束求解器来解决斑马难题的练习，我尝试使用Prolog clpfd library。

我知道在 Prolog 中还有其他更惯用的方法来解决这个问题，但这个问题专门针对 clpfd 包！

所以我要解决的难题的具体变体（鉴于其中有很多）是这个：

有五间房子

英国人住在红房子里 瑞典人养狗 丹麦人喜欢喝茶 温室留给白宫 温室的主人喝咖啡 抽 Pall Mall 的人拥有一只鸟 中间屋喝牛奶 黄房子的主人抽登喜路 挪威人住在第一所房子里 万宝路吸烟者住在猫主人旁边 马主住在抽登喜路的人旁边 温菲尔德吸烟者喜欢喝啤酒 挪威人住在蓝房子旁边 德国人抽罗斯曼烟 万宝路吸烟者有一个喝水的邻居

我尝试用以下方法解决：

房子可以拥有的每个属性都被建模为一个变量，例如“英国”， “狗”、“绿色”等。属性可以取值从 1 到 5，具体取决于房子 它们发生的地方，例如如果变量“Dog”取值 3，则狗住在 第三宫。

这种方法可以很容易地模拟这样的邻居约束：

def neighbor(X, Y) :-
    (X #= Y-1) #\/ (X #= Y+1).

但不知何故，clpfd 包并没有产生解决方案，即使 (IMO) 问题已正确建模（我使用与 Choco constraint solver 完全相同的模型，结果是正确的）。

完整代码如下：

:- use_module(library(clpfd)).

neighbor(X, Y) :-
    (X #= (Y - 1)) #\/ (X #= (Y + 1)).

solve([British, Swedish, Danish, Norwegian, German], Fish) :-

    Nationalities = [British, Swedish, Danish, Norwegian, German],
    Colors = [Red, Green, Blue, White, Yellow],
    Beverages = [Tea, Coffee, Milk, Beer, Water],
    Cigarettes = [PallMall, Marlboro, Dunhill, Winfield, Rothmanns],
    Pets = [Dog, Bird, Cat, Horse, Fish],

    all_different(Nationalities),
    all_different(Colors),
    all_different(Beverages),
    all_different(Cigarettes),
    all_different(Pets),

    Nationalities ins 1..5,
    Colors ins 1..5,
    Beverages ins 1..5,
    Cigarettes ins 1..5,
    Pets ins 1..5,

    British #= Red, % Hint 1
    Swedish #= Dog, % Hint 2
    Danish #= Tea, % Hint 3

    Green #= White - 1 , % Hint 4
    Green #= Coffee, % Hint 5,
    PallMall #= Bird, % Hint 6

    Milk #= 3, % Hint 7
    Yellow #= Dunhill, % Hint 8,
    Norwegian #= 1, % Hint 9

    neighbor(Marlboro, Cat), % Hint 10
    neighbor(Horse, Dunhill), % Hint 11
    Winfield #= Beer, % Hint 12

    neighbor(Norwegian, Blue), % Hint 13
    German #= Rothmanns, % Hint 14,
    neighbor(Marlboro, Water). % Hint 15

我是否误解了clpfd 中的一个概念，或者我只是在这里遗漏了一些明显的东西？如果有帮助，here 您可以找到使用 Choco 和 Scala 实现的相同方法。

---

编辑：我认为求解器无法解决问题的原因在于它从来没有为变量提供明确的值，而只是提供范围，例如“鱼 1..3\/5”。

【问题讨论】：

使用 label(Vars) 或 labeling(Options, Vars) 来解决问题。

"label" 仅在有明确结果时才有效，而我为每个变量得到的只是范围（如编辑中所述）。

如果您的 CLP(FD) 将具有“Expr in Set”，那么可以将neighbor(X,Y) :- X - Y in [-1,1] 形式化。

你可以定义 neighbour/2 为：abs(X-Y) #= 1.

@CookieMonster：你可以写V in -1\/1，但允许第一个参数的表达式会使其成为默认值。

【参考方案1】：

这里有几个误解：您说“clpfd 包没有产生解决方案”，但实际上它确实产生了一个：

?- solve(Ls, Fish), label(Ls).
Ls = [3, 5, 2, 1, 4],
Fish in 1\/4,
all_different([5, 3, _G3699, 2, Fish]),
_G3699 in 1\/4,
_G3699+1#=_G3727,
_G3741+1#=_G3699,
_G3727 in 2\/4..5,
2#=_G3727#<==>_G3766,
_G3766 in 0..1,
_G3792#\/_G3766#<==>1,
_G3792 in 0..1,
2#=_G3741#<==>_G3792,
_G3741 in 0\/2..3.

所以我们知道如果有解，那么 Fish 要么是 1 要么是 4。让我们试试 1：

?- solve(Ls, Fish), label(Ls), Fish = 1.
false.

没有。那么让我们试试4：

?- solve(Ls, Fish), label(Ls), Fish = 4.
Ls = [3, 5, 2, 1, 4],
Fish = 4.

这是可行的，并且是解决问题的基础解决方案。您可以通过不同的方式获得它，例如将 Fish 包含在要标记的变量中：

?- solve(Ls, Fish), label([Fish|Ls]).
Ls = [3, 5, 2, 1, 4],
Fish = 4 ;
false.

标记的目的正是为受约束的变量尝试具体值，而与是否确实存在解决方案无关。巧合的是，在这种情况下， all_distinct/1 足够强大，可以自己产生一个基本解决方案，但一般情况下当然不是这样，您最终必须使用标签来获得无条件（即没有更多未决约束）的答案。当然，您通常还必须标记您感兴趣的所有变量，而不是像最初那样标记它们的子集。要标记单个变量，您可以使用 indomain/1，因此将 indomain(Fish) 附加到上面的第一个查询也可以。我无法重现您在进一步评论中提到的实例化错误，事实上，正如您在上面看到的，最通用的查询 solve(X, Y) 适用于您发布的代码。最后，看看这个：

neighbor(X, Y) :- abs(X-Y) #= 1.

【参考方案2】：

在 SWI-Prolog 中运行你的代码，我明白了

?- solve(X),label(X).
X = [3, 5, 2, 1, 4].

没有label：

?- solve(X).
X = [3, _G3351, _G3354, 1, _G3360],
_G3351 in 4..5,
all_different([_G3351, _G3386, _G3389, 2, _G3395]),
all_different([3, _G3351, _G3354, 1, _G3360]),
_G3386 in 3..5,
all_different([_G3386, _G3444, 1, _G3450, _G3360]),
_G3389 in 1\/3..5,
_G3389+1#=_G3478,
_G3492+1#=_G3389,
_G3395 in 1\/3..5,
_G3478 in 2..6,
_G3444#=_G3478#<==>_G3529,
_G3444 in 2..5,
_G3444#=_G3556#<==>_G3553,
_G3444#=_G3568#<==>_G3565,
_G3444#=_G3492#<==>_G3577,
_G3450 in 2\/5,
all_different([_G3354, 4, 3, _G3450, _G3614]),
_G3360 in 2\/4..5,
_G3354 in 2\/5,
_G3614 in 1..2\/5,
_G3614+1#=_G3556,
_G3568+1#=_G3614,
_G3556 in 2..3\/6,
_G3553 in 0..1,
_G3565#\/_G3553#<==>1,
_G3565 in 0..1,
_G3568 in 0..1\/4,
_G3492 in 0..4,
_G3577 in 0..1,
_G3577#\/_G3529#<==>1,
_G3529 in 0..1.

如果我将 all_different 更改为 all_distinct 我会得到没有标签的解决方案：

....
all_distinct(Nationalities),
all_distinct(Colors),
all_distinct(Beverages),
all_distinct(Cigarettes),
all_distinct(Pets),
....

?- solve(X).
X = [3, 5, 2, 1, 4].

如您所见，文档声明 all_distinct 与 all_different 的传播更强。运行建议的示例有助于了解它们之间的区别：

?- maplist(in, Vs, [1\/3..4, 1..2\/4, 1..2\/4, 1..3, 1..3, 1..6]), all_distinct(Vs).
false.

?- maplist(in, Vs, [1\/3..4, 1..2\/4, 1..2\/4, 1..3, 1..3, 1..6]), all_different(Vs).
Vs = [_G419, _G422, _G425, _G428, _G431, _G434],
_G419 in 1\/3..4,
all_different([_G419, _G422, _G425, _G428, _G431, _G434]),
_G422 in 1..2\/4,
_G425 in 1..2\/4,
_G428 in 1..3,
_G431 in 1..3,
_G434 in 1..6.

【讨论】：

all_distinct 成功了。谢谢。我一直在尝试做类似solve(X,Y) 的事情（请参阅更新的求解签名），我得到了ERROR: Arguments are not sufficiently instantiated，但使用all_distinct 时不会发生这种情况。

乍一看，我注意到 Fish 在原始代码中是一个单例，但修改代码我没有得到你正确发现的后果。

在我测试的所有情况下，

all_distinct 都比all_different 慢得多，然后是label。

@fpg1503：我从未对它们进行基准测试。如果您有一些可发布的示例，绘制两种算法的“强度”增强与增强复杂度的图表可能会很有趣