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的方式写成。

盖瑟先生建议我把谓词(关系)保持简短。实例的这种编码的问题是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还建议，求解者(clasp)也可以从用另一种方式编写的规则中获益：

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

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

为了获得更好的输出，您可以创建一个像house/6那样提供输出的关系。

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