斑马拼图- Clingo:断言部分约束

Question

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

五个不同国籍的男人住在五个相邻的房子里，每个房子的颜色都不同;他们都有不同的工作，喜欢的动物和喜欢的饮料。我们知道:

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

作业是找出谁喜欢斑马。所以我开始断言:

% 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).

现在我坚持断言约束;如何编写断言代码?通过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的输出)是巨大的。您可以在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).
...

并从那里开始。现在元素的密度只有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，它们不是最新的版本。如果您使用了新的clingo，则可能需要进行一些修改。