斑马谜题真值表

Question

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

Answer 1

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

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

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

Answer 2

一个典型的谜语可以看成是一个 k×n 矩阵，然后用 k×n² 个布尔变量（如 here）进行编码。假设变量 P_ijm 为真，当且仅当 - 矩阵中的 (i,j)-entry 具有值 m。

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

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

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

Answer 3

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

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

可以找到更优雅的版本here。它表现出相同数量的决策变量。

%  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];

Answer 4

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

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

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