斑马谜题真值表
Posted
技术标签:
【中文标题】斑马谜题真值表【英文标题】:Truth table for the zebra puzzle 【发布时间】:2017-10-20 04:42:20 【问题描述】:我正在阅读“计算机科学提炼”一书,但遇到了麻烦。作者建议通过真值表解决爱因斯坦的“斑马难题”,但我不知道如何。我找不到起始条件和变量。你对最小的桌子有什么想法吗?我想我只能创建一个 6^6 版本
【问题讨论】:
【参考方案1】:我是 OP 提到的书的作者。我的意思不是让读者只使用一个大的真值表来解决斑马谜题,而是把它作为一种工具来检测永远不会发生的情况,并更好地指导探索过程。
使用包含代表房屋/属性状态的变量的大型真值表,您可以发现一个变量,如果该变量为真,则意味着许多相关状态。最好测试这些变量以找出逻辑矛盾,而不是简单地对所有变量进行暴力破解。
我写了一篇详细的博客文章,解释了如何仅使用简单的推理和布尔代数来解决斑马难题,这里:https://code.energy/solving-zebra-puzzle/
【讨论】:
【参考方案2】:一个典型的谜语可以看成是一个 k×n 矩阵,然后用 k×n2 个布尔变量(如 here)进行编码。假设变量 Pijm 为真,当且仅当 - 矩阵中的 (i,j)-entry 具有值 m。
显然,您需要一个 SAT 解算器来解开以这种方式编码的谜语。我想作者建议您使用真值表只是出于讽刺,或者出于教学原因,或者他/她要求您实施 SAT 求解器中使用的技术。
为了减少所涉及的“术语”的数量,必须在一阶逻辑的(可判定的)片段中对这个难题进行建模,例如喇叭子句(Prolog)或描述逻辑(OWL 推理器)。
这种术语数量的“命题爆炸”的另一个例子是命题鸽巢原则。
【讨论】:
【参考方案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];
【讨论】:
【参考方案4】:看看我为puzzle-solvers 包编写的代码。它是为了在 SO 上解决一个类似的问题。由于它是一个非常小的包,您可能可以很容易地看到代码是如何编写的。
代码是Solver
类,它维护一个值矩阵,并提供建立关系所需的方法,这些关系会自动修剪矛盾边的底层图。
您可以按照docs 中的逻辑详细说明进行操作。这真正解释了如何使用图的矩阵表示来记录规则中的关系。它的要点是,每条规则要么在两个类别之间建立直接联系,从而修剪所有矛盾的边缘,要么消除边缘,这也具有含义。
【讨论】:
以上是关于斑马谜题真值表的主要内容,如果未能解决你的问题,请参考以下文章