Clingo：断言部分约束

Question

我正在尝试在clingo 中实现一个程序，该程序解决了其中一个经典谜题，其中您有一系列事实和约束的断言，并且您必须推断出其他事实。问题来了：

五个不同国籍的男人住在五个并排的房子里，每个房子都有不同的颜色；他们都有不同的工作，不同的喜爱动物和喜爱的饮料。我们知道：

1. 英国人住在红房子里。
2. 西班牙男人最喜欢的动物是狗。
3. 日本人是画家。
4. 意大利男人喝茶。
5. 挪威男子住在左起第一个房子里。 (number_norw = 1)
6. 住在温室里的人喝咖啡。
7. 绿色房子就在白色房子的右边。 (number_green = number_white + 1)
8. 店员喜欢猫。
9. 推销员住在黄房子里。
10. 牛奶是中心屋最受欢迎的饮品。 (number_milk = 3)
11. 挪威人的房子与蓝色的房子相邻。 (number_norw = number_blue ± 1)
12. 厨师喜欢果汁。
13. 住在医生旁边房子里的男人喜欢狐狸。
14. 爱马的男人住在推销员的隔壁。

任务是找出谁喜欢斑马。 所以我提出断言：

% Number (the number of the house, 1 being the leftmost of the block, 5 the rightmost)
number(1..5).

% Color
color(red;green;white;yellow;blue).

% Nationality
nationality(english;spanish;japanese;italian;norwegian).

% Animal
animal(dog;cat;fox;horse;zebra).

% Job
job(painter;clerk;salesman;cook;doctor).

% Beverage
beverage(tea;coffee;milk;juice;coke).

% House
house(X, C, N, A, J, B) :-
    number(X),
    color(C),
    nationality(N),
    animal(A),
    job(J),
    beverage(B).

现在我坚持断言约束；如何编码断言 1. 到 14.？我只需要了解正确的语法，所以如果有人可以通过一两个示例让我走上正确的轨道，我可以弄清楚其余的。 谢谢。

注意请注意，我可以从 5. 和 11. 推断出第二个房子是蓝色的，因为11. number_blue = number_norw ± 1、5. number_norw = 1 和 0 不在可能的数字范围内，但我不想手动添加因为我希望clingo 自己解决它。

Answer 1

为第一个断言添加约束的一种方法：

% 1. The English man lives in the red house.
%     S: english --> red house <==> red house OR not english
% not S: not (red house OR not english) <==> not red house AND english
% ie. it is not so, that the english man doesn't live in the red house
:- not 1 { house(X, red, english, A, J, B) :
           number(X) : animal(A) : job(J) : beverage(B) }.

作为另一个例子，第七个断言：

% 7. The green house is immediately right of the white one.
% (number_green = number_white + 1)
:- house(NG, green, _, _, _, _), house(NW, white, _, _, _, _), NG!=NW+1.

然而，这将导致求解时间长和内存需求大（千兆字节），因为接地程序（外国佬的输出）非常庞大。您可以通过gringo -t yourcode.asp 看到这一点。这是因为“不关心”变量_（以及上面第一个断言的约束中的X, A, J, B）。每条规则将至少以 5*5*5*5 的方式编写。

M. Gebser 建议我谓词（关系）应该保持简短。这种实例编码的问题是house/6 太长了。解决此问题的一种方法是将其编码为以下样式：

house(1..5).
elem(color, red;green;white;yellow;blue).
elem(nationality, english;spanish;japanese;italian;norwegian).
...

并从那里开始。现在 elem 的数量只有 2。当以这种方式定义实例时，程序变得更简单，例如。断言的约束不需要聚合（1{ ... }N 语法）。

:- not chosen(H, nationality, english), chosen(H, color, red).

M. Gebser 还建议求解器（扣环）也可能受益于以另一种方式编写的规则：

:- not chosen(H, nationality, english), chosen(H, color, red).
:- chosen(H, nationality, english), not chosen(H, color, red).

您还需要一些额外的限制，例如不应将同一类型的两个不同元素映射到一个房子。

为了获得更好的输出，您可以建立一个关系，使输出类似于 house/6 那样。

请注意，我使用了 gringo3 和 clasp2，它们不是最新版本。如果您有新的 clgo，可能需要进行修改。