prolog - 使用 clpfd Prolog 库解决斑马拼图(又名爱因斯坦拼图)

Question

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

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

所以我试图解决的谜题的具体变化(假设有很多)是这个:

有五个房子

英国人住红房子

瑞典人养狗

丹麦人喜欢喝茶

绿屋留给白屋

温室主人喝咖啡

抽Pall Mall的人拥有一只鸟

中家喝牛奶

黄屋屋主抽Dunhill烟

挪威人住第一间房子

万宝路吸烟者住在猫主人旁边

马主住在抽dunhill的人旁边

winfield吸烟者喜欢喝啤酒

挪威人住在蓝房子旁边

德国人抽罗斯曼烟

万宝路烟民有个邻居喝水

我试图用以下方法解决它:

Each attribute a house can have is modeled as a variable, e.g. "British", "Dog", "Green", etc. The attributes can take values from 1 to 5, depending on the house in which they occur, e.g. if the variable "Dog" takes the value 3, the dog lives in the third house.

这种方法可以很容易地对像这样的邻居约束进行建模:

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”。

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.