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.？我只需要理解正確的語法，所以如果有人可以用一兩個例子讓我走上正確的軌道，我可以找出其他的例子。 謝謝。

N.B.注意我可以從5和11推斷出第二座房子是藍色的，因爲11. number_blue = number_norw ± 1,5. number_norw = 1和0不在可能的數字範圍內，但我不想將它手動添加到約束因爲我預計clingo自己弄明白了。

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

而作爲另一實例第七assertation：加約束的第一assertation

Answer 1

一種方式

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

並從那裏開始。現在elem的arity只有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。如果您有新的粘貼物，可能需要進行修改。