解决使用clpfd的Prolog库中的斑马谜（又名爱因斯坦的难题）(Solving the Zebr

我一直在考虑一项工作，解决使用我选择的约束求解斑马拼图，我试了一下使用的Prolog clpfd库。

据我所知，还有其他更地道的方式来解决Prolog的这个问题，但这个问题是专门关于clpfd包！

所以这一难题的具体变化（因为有很多他们的）我试图解决是这个：

有五个房子

英国人住在红房子
瑞典拥有一只狗
丹麦喜欢喝茶
绿房子留给白宫
绿房子的主人喝咖啡
该抽Pall Mall香烟的人拥有一只鸟
牛奶是在中间的房子醉
黄色房子主人抽Dunhill香烟
挪威人住在第一间房子
万宝路吸烟者住旁边的猫主人
马主人住旁边，谁抽Dunhill香烟的人
温菲尔德吸烟者喜欢喝啤酒
挪威人住在蓝房子
德国烟雾rothmanns
万宝路吸烟者有一个邻居谁喝的水

我试着用以下的方法来解决这个问题：

每个属性房子可以都被建模为可变，例如“英国”，“狗”，“绿色”，等等的属性可以取的值从1到5，这取决于在它们发生的房子，例如，如果可变“狗”取值3，狗住在第三宫。

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

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

但不知何故， clpfd包不产生一个解决方案，即使（IMO）的问题是正确建模（我用的是完全一样的模型与巧克力约束求解，结果是正确的）。

下面是完整的代码：

:- 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 ，还是我只是缺少明显的东西吗？如果有帮助，在这里你可以找到用巧克力和Scala实现相同的方法。

编辑：为什么我相信求解是解决不了问题的IST它永远不会来作为变量的确定值出现，但只有在范围内的原因，如“鱼1..3 \ / 5”。

Answer 1:

在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 VS 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.

Answer 2:

这里有几个误区：幽州“的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.

因此，我们知道，如果有一个解决方案，那么鱼或者是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.

这个工程，是一个地解决问题。您可以通过鱼将被标记为变量得到它以不同的方式，例如：

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

标志的目的正是要尝试约束变量，独立的是否真的是有解决方案的具体数值。巧合的是，all_distinct / 1够强本身在这种情况下，产生地面的解决方案，但一般这个是当然的情况下不和你最后必须使用标签来获得无条件的（即没有更多等待约束）的答案。当然，你必须那么一般也标注是你感兴趣的所有变量，而不是其中的一个子集，你做了最初。要标记一个变量，你可以使用indomain / 1，所以追加indomain（鱼）到第一上面的查询也将工作。我无法重现你进一步的评论中提到的实例错误，其实你看到的最普通的查询解决以上（X，Y）的作品与你发布的代码。最后，检查了这一点：