解决斑马难题(又名。)使用clpfd Prolog库

Question

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

我知道在Prolog中有其他更多的惯用方法来解决这个问题，但是这个问题是关于clpfd 软件包！的。

因此，我试图解决的难题的具体变化(考虑到其中的很多)是这样一个：

有五栋房子，

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

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

房屋可以拥有的每一个属性都被建模为一个变量。"British“、" dog”、"Green“等属性的值可以从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实现的相同方法。

编辑:我认为求解者不能解决问题的原因是，它从来没有给出变量的确定值，而是只给出了范围。“鱼类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。

?- 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在这种情况下本身就足够强，但是通常情况不是这样，您最终必须使用标号来获得无条件的(即不再有悬而未决的约束)答案。当然，在一般情况下，您还必须标记所有您感兴趣的变量，而不仅仅是它们的子集，正如您最初所做的那样。要标记单个变量，您可以使用域内/1，因此在上面的第一个查询中附加域内(Fish)也是可行的。我无法重现您在进一步的注释中提到的实例化错误，事实上，正如您在上面看到的，最通用的查询解决(X，Y)与您发布的代码一起工作。最后，看看这个：

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