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

Question

我已经使用我选择的约束求解器进行了练习来解决斑马拼图,我尝试使用Prolog clpfd库.

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

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

有五个房子

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

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

房屋可以具有的每个属性被建模为变量,例如"英国","狗","绿色"等.属性可以取1至5的值,具体取决于它们出现的房屋,例如,如果变量"狗"取值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)附加到上面的第一个查询也可以.我无法重现您在进一步评论中提到的实例化错误,事实上如上所述,最常见的查询求解(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_distinctvs更强的传播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.