解决斑马之谜(又名.爱因斯坦拼图)使用clpfd Prolog库

Question

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

我知道在 Prolog 中还有其他更惯用的方法可以解决这个问题，但这个问题是专门关于clpfd包的！

因此，我试图解决的难题的具体变化（鉴于其中有很多）是这样的：

有五栋房子

1. 英国人住在红房子里
2. 瑞典人养了一只狗
3. 丹麦人喜欢喝茶
4. 温室留给白宫
5. 温室主人喝咖啡
6. 抽烟的人拥有一只鸟
7. 牛奶在中屋喝
8. 黄房子的主人抽登喜路
9. 挪威人住在第一所房子里
10. 万宝路吸烟者住在猫主人旁边
11. 马主人住在抽登喜路的人旁边
12. 温菲尔德吸烟者喜欢喝啤酒
13. 挪威人住在蓝房子旁边
14. 德国人抽罗斯曼
15. 万宝路吸烟者有一个喝水的邻居

我尝试使用以下方法解决它：

房子可以具有的每个属性都被建模为一个变量，例如"英国"， "狗"、"绿色"等。属性可以取 1 到 5 之间的值，具体取决于房屋 它们出现的地方，例如，如果变量"Dog"取值 3，则狗生活在 第三宫。

此方法可以轻松对相邻约束进行建模，如下所示：

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

但不知何故，clpfd包没有产生解决方案，即使（IMO）问题建模正确（我在Choco约束求解器中使用了完全相同的模型，结果是正确的）。

以下是完整的代码：

:- 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中的一个概念，或者我只是在这里错过了一些明显的东西？ 如果它有帮助，在这里你可以找到使用Choco和Scala实现的相同方法。

---

编辑：我认为求解器无法解决问题的原因是它从未为变量提出明确的值，而只是范围，例如"Fish 1..3\/5"。

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

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