3

我正在阅读“计算机科学提炼”一书，但遇到了麻烦。作者建议通过真值表解决爱因斯坦的“斑马谜题”，但我不知道如何解决。我找不到起始条件和变量。你对最小的桌子有什么想法吗？我想我只能创建一个 6^6 版本

4

4 回答 4

4

我是OP提到的书的作者。我的意思不是让读者只使用一个大的真值表来解决斑马谜题，而是将它作为一种工具来检测永远不会发生的情况，并更好地指导探索过程。

使用带有代表房屋/属性状态的变量的大真值表，您可以发现一个变量，如果为真，则意味着许多相关状态。最好测试这些变量以发现逻辑矛盾，而不是简单地暴力破解所有变量。

我写了一篇详细的博客文章，解释如何仅使用简单的推理和布尔代数来解决斑马难题，这里：https ://code.energy/solving-zebra-puzzle/

于 2017-05-26T17:35:53.840 回答
1

一个典型的谜语可以看作是 ak×n 矩阵，然后用 k×n 2 个布尔变量编码，就像这里一样。当且仅当矩阵中的 (i,j) 项具有值 m 时，考虑变量 P ijm为真。

显然，您需要一个 SAT 求解器来解决以这种方式编码的谜语。我想作者只是讽刺地建议您使用真值表，或者出于教学原因，或者他/她要求您实施 SAT 求解器中使用的技术。

为了减少涉及的“术语”的数量，必须将这个难题建模为一阶逻辑的（可判定的）片段，例如霍恩子句（Prolog）或描述逻辑（OWL 推理器）。

术语数量的这种“命题爆炸”的另一个例子是命题鸽巢原则。

于 2017-05-20T07:52:28.723 回答
0

下面的MiniZinc脚本显示了如何根据25决策变量对斑马拼图进行编码。它们每个都有一个值 1..5。就布尔变量而言，25*3 = 75将需要位。

@Stanislav Kralin 建议的直接布尔编码需要5*5*5 = 125布尔决策变量。

可以在这里找到更优雅的版本。它展示了相同数量的决策变量。

%  Zebra Puzzle in MiniZinc
%  https://en.wikipedia.org/wiki/Zebra_Puzzle

%  for all_different()
include "globals.mzn";

%  Number of houses (cf. constraint 1.)
int: n = 5;
set of int: House = 1..5;

%  Nationalities
var House: English;
var House: Spaniard;
var House: Ukranian;
var House: Norwegian;
var House: Japanese;

%  Beverages
var House: Coffee;
var House: Tea;
var House: Milk;
var House: Orange_Juice;
var House: Water;

%  Pets
var House: Dog;
var House: Horse;
var House: Snail;
var House: Fox;
var House: Zebra;

%  House colors
var House: Red;
var House: Yellow;
var House: Ivory;
var House: Blue;
var House: Green;

%  Cigarette brands
var House: Old_Gold;
var House: Kools;
var House: Chesterfield;
var House: Lucky_Strike;
var House: Parliaments;

%  Explicit constraints
% 1. There are five houses.

% 2. The Englishman lives in the red house.
constraint English = Red;

% 3. The Spaniard owns the dog.
constraint Spaniard = Dog;

% 4. Coffee is drunk in the green house.
constraint Coffee = Green;

% 5. The Ukranian drinks tea.
constraint Ukranian = Tea;

% 6. The green house is immediately to the right of the ivory house.
constraint Green = (Ivory + 1);

% 7. The Old Gold smoker owns snails.
constraint Old_Gold = Snail;

% 8. Kools are smoked in the yellow house.
constraint Kools = Yellow;

% 9. Milk is drunk in the middle house.
constraint Milk = (n + 1)/2;

% 10. The Norwegian lives in the first house.
constraint Norwegian = 1;

% 11. The man who smokes Chesterfields lives in the house next to the man with the fox.
constraint abs(Chesterfield - Fox) = 1;

% 12. Kools are smoked in the house next to the house where the horse is kept.
constraint abs(Kools - Horse) = 1;

% 13. The Lucky Strike smoker drinks orange juice.
constraint Lucky_Strike = Orange_Juice;

% 14. The Japanese smokes Parliaments.
constraint Japanese = Parliaments;

% 15. The Norwegian lives next to the blue house.
constraint abs(Norwegian - Blue) = 1;

%  Implicit constraints
%  each of the five houses is painted a different color
constraint all_different([Red, Blue, Yellow, Green, Ivory]);

%  inhabitants are of different national extractions
constraint all_different([English, Spaniard, Ukranian, Norwegian, Japanese]);

%  inhabitants own different pets
constraint all_different([Dog, Horse, Snail, Fox, Zebra]);

%  inhabitants drink different beverages 
constraint all_different([Coffee, Tea, Milk, Orange_Juice, Water]);

%  inhabitants smoke different brands of American cigarets [sic]
constraint all_different([Old_Gold, Kools, Chesterfield, Lucky_Strike, Parliaments]);

solve satisfy;

function string: take(int: h, array[1..n-1] of House: x, array[House] of string: s) =
  if x[1] = h then s[1] 
  elseif x[2] = h then s[2] 
  elseif x[3] = h then s[3] 
  elseif x[4] = h then s[4] 
  else s[5] endif;

output ["\nColor       "] ++
       [ take(h, [fix(Red), fix(Blue), fix(Green), fix(Ivory)], 
                 ["red          ", "blue         ", "green        ", "ivory        ", "yellow       "])| h in House] ++
       ["\nNationality "] ++
       [ take(h, [fix(English), fix(Spaniard), fix(Ukranian), fix(Norwegian)],
                 ["English      ", "Spaniard     ", "Ukranian     ", "Norwegian    ", "Japanese     "])| h in House] ++
       ["\nPet         "] ++
       [ take(h, [fix(Dog), fix(Horse), fix(Snail), fix(Fox)],
                 ["Dog          ", "Horse        ", "Snail        ", "Fox          ", "Zebra        "])| h in House] ++
       ["\nBeverage    "] ++
       [ take(h, [fix(Coffee), fix(Tea), fix(Milk), fix(Orange_Juice)],
                 ["Coffee       ", "Tea          ", "Milk         ", "Orange Juice ", "Water        "])| h in House] ++
       ["\nCigarette   "] ++
       [ take(h, [fix(Old_Gold), fix(Kools), fix(Chesterfield), fix(Lucky_Strike)],
                 ["Old Gold     ", "Kools        ", "Chesterfield ", "Lucky Strike ", "Parliaments  "])| h in House];
于 2017-05-20T16:59:59.327 回答
0

看看我为解谜程序包编写的代码。它是为了在 SO 上解决一个类似的问题。由于它是一个非常小的包，您可能可以很容易地看到代码是如何编写的。

代码是Solver类，它维护一个值矩阵，并提供建立关系所需的方法，这些关系自动修剪矛盾边的底层图。

您可以按照文档中的逻辑详细说明进行操作。这真正解释了如何使用图的矩阵表示来记录规则中的关系。它的要点是，每条规则要么在两个类别之间建立直接联系，从而修剪所有矛盾的边缘，要么消除边缘，这也具有含义。

于 2022-01-10T11:06:14.593 回答