命题客厅谜题：使用 Propositional Logic 解决谜题
NULL BITMAP by Justin Jaffray
Subscribe Archives April 21, 2025
Propositional Parlor Puzzle
× Close dialog NULL BITMAP.png
× Close dialog image.png
最近我在玩 Blue Prince，如果你喜欢像 Return of the Obra Dinn 或 Outer Wilds 这样的解谜游戏，并且也是像 Slay the Spire 这样的肉鸽游戏的爱好者，这会是一段美好的时光。
游戏中的一个房间，客厅 (Parlor)，包含一个逻辑谜题，每次运行都会有所不同。在这篇文章中，我们将对这些谜题进行建模和分析。有些人可能会认为这是剧透！
在客厅里，有三个盒子：一个蓝色的盒子、一个白色的盒子和一个黑色的盒子。每个盒子都会说出一些陈述。我们还给出了以下规则：
- 总是至少有一个盒子只说真话。
- 总是至少有一个盒子只说假话。
- 奖品恰好在一个盒子里。
× Close dialog image.png
这是一个谜题的例子：
Blue: You are in the parlor
White: This box is empty
Black: The blue box is true
蓝色盒子说的是一个显而易见的事实——盒子游戏总是发生在客厅里。因此，黑色盒子也在说真话，因为蓝色盒子说的是真话。由于我们根据规则知道必须至少有一个盒子说_假_话，所以只能是白色盒子，因此我们可以推断出白色盒子_不_是空的，并且有奖品。
有时谜题会变得更加棘手。考虑一下：
Blue: the gems are in a box with a true statement
White: the gems are in a box with a false statement
Black: The white box is true
这里实际上有两种一致的解释：
Blue: true
White: false
Black: false
和
Blue: false
White: true
Black: true
都是有效的。诀窍不在于确定哪个盒子在说真话，而是奖品在哪里，在这种情况下，任何一种解释都表明奖品在蓝色盒子中。
让我们创建一个自动解决这些谜题的工具！如果，比如说，你正在制作这个游戏并且编写了很多谜题，并且想要某种机械保证作为测试套件的一部分，以确保你没有犯错，这可能会很有用。
我们可以使用 Propositional Logic 来表示这些谜题。这是一种对特定陈述的真实性感兴趣的逻辑。你可以把它想象成只包含 bool 类型值的表达式。我们通常在 Propositional Logic 中有四种对象：
- 变量，例如
foo、bar。 - negations （否定），它接受一个值并将结果从真变为假，或从假变为真。
- disjuncts （析取），即多个其他对象之间的
OR运算。 - conjuncts （合取），即多个其他对象之间的
AND运算。
我们可以用 ColdOutside 和 ShouldWearACoat 的变量来符号化表示像“外面很冷，你应该穿外套”这样的表达式，写作 ColdOutside AND ShouldWearACoat。身体强壮的人可能不需要穿外套，所以我们可以写成 ColdOutside AND (ShouldWearACoat OR IsTough)。
我们经常感兴趣的是，给定这样一个表达式：
- 是否存在 对变量的真/假赋值，使表达式为真？
- 所有 使赋值为真的变量的真/假赋值是什么？
这个问题被称为 SAT，代表 "satisfiability"（可满足性）。我们询问给定的表达式是否可满足。作为一个简单的例子，表达式 A AND (NOT A) 是_不可_满足的。
SAT 求解是一个深入的话题，并且有很多用于解决 SAT 问题的花哨而强大的工具。幸运的是，我们不需要所有的这些机制，我们的表达式将会足够简单，我们可以直接暴力破解它们，这很好，因为自己做这些事情更有趣。
让我们首先提出一种表示真、假和变量的方法（请原谅我的 JavaScript 风格，我已经大约十年没有专业地编写它了）：
constTrue = { type: 'true' };
constFalse = { type: 'false' };
constVar = (name) => ({
type: 'var',
name,
});
我们可以使用它来提出我们将需要的所有变量来表示这些问题：
constBlueBoxIsTrue = Var('BlueBoxIsTrue');
constWhiteBoxIsTrue = Var('WhiteBoxIsTrue');
constBlackBoxIsTrue = Var('BlackBoxIsTrue');
constBlueBoxIsFalse = Var('BlueBoxIsFalse');
constWhiteBoxIsFalse = Var('WhiteBoxIsFalse');
constBlackBoxIsFalse = Var('BlackBoxIsFalse');
constBlueBoxHasGems = Var('BlueBoxHasGems');
constWhiteBoxHasGems = Var('WhiteBoxHasGems');
constBlackBoxHasGems = Var('BlackBoxHasGems');
我们为盒子为真和为假分别设置了变量，因为如果一个盒子做出了多个陈述，它不一定是真或假：它可以有一个是真的而一个是假的，那么这个盒子本身就不是“真”或“假”。
接下来我们需要我们的运算符，And，Or和Not。
constAnd = (...terms) => {
return {
type: 'and',
terms,
};
};
constOr = (...terms) => {
return {
type: 'or',
terms,
};
};
constNot = (term) => {
return {
type: 'not',
term,
};
};
现在我们可以用这些来构建更复杂的表达式来表示我们游戏中的规则。
记住，至少有一个盒子是“真”，并且至少有一个盒子是“假”：
constOneBoxIsTrue = Or(
BlueBoxIsTrue,
WhiteBoxIsTrue,
BlackBoxIsTrue,
);
constOneBoxIsFalse = Or(
BlueBoxIsFalse,
WhiteBoxIsFalse,
BlackBoxIsFalse,
);
宝石恰好在一个盒子里：
constGemsOnlyInOneBox = Or(
And(
BlueBoxHasGems,
Not(WhiteBoxHasGems),
Not(BlackBoxHasGems),
),
And(
Not(BlueBoxHasGems),
WhiteBoxHasGems,
Not(BlackBoxHasGems),
),
And(
Not(BlueBoxHasGems),
Not(WhiteBoxHasGems),
BlackBoxHasGems,
),
);
我们可以将所有这些组合起来以获得我们游戏的基本规则：
constBaseRules = And(
GemsOnlyInOneBox,
OneBoxIsTrue,
OneBoxIsFalse,
);
{
type: 'and',
terms: [
{
type: 'or',
terms: [
{
type: 'and',
terms: [
{ type: 'var', name: 'BlueBoxHasGems' },
{
type: 'not',
term: { type: 'var', name: 'WhiteBoxHasGems' },
},
{
type: 'not',
term: { type: 'var', name: 'BlackBoxHasGems' },
},
],
},
{
type: 'and',
terms: [
{
type: 'not',
term: { type: 'var', name: 'BlueBoxHasGems' },
},
{ type: 'var', name: 'WhiteBoxHasGems' },
{
type: 'not',
term: { type: 'var', name: 'BlackBoxHasGems' },
},
],
},
{
type: 'and',
terms: [
{
type: 'not',
term: { type: 'var', name: 'BlueBoxHasGems' },
},
{
type: 'not',
term: { type: 'var', name: 'WhiteBoxHasGems' },
},
{ type: 'var', name: 'BlackBoxHasGems' },
],
},
],
},
{
type: 'or',
terms: [
{ type: 'var', name: 'BlueBoxIsTrue' },
{ type: 'var', name: 'WhiteBoxIsTrue' },
{ type: 'var', name: 'BlackBoxIsTrue' },
],
},
{
type: 'or',
terms: [
{ type: 'var', name: 'BlueBoxIsFalse' },
{ type: 'var', name: 'WhiteBoxIsFalse' },
{ type: 'var', name: 'BlackBoxIsFalse' },
],
},
],
}
嗯。有点丑。我们可以编写一个助手来更漂亮地打印这些。
((BlueBoxHasGems ∧ ¬WhiteBoxHasGems ∧ ¬BlackBoxHasGems) ∨ (¬BlueBoxHasGems ∧ WhiteBoxHasGems ∧ ¬BlackBoxHasGems) ∨ (¬BlueBoxHasGems ∧ ¬WhiteBoxHasGems ∧ BlackBoxHasG
ems))
∧ (BlueBoxIsTrue ∨ WhiteBoxIsTrue ∨ BlackBoxIsTrue)
∧ (BlueBoxIsFalse ∨ WhiteBoxIsFalse ∨ BlackBoxIsFalse)
好多了！这里使用了 ∧ 表示 AND，∨ 表示 OR，以及 ¬ 表示 NOT 的典型符号。
让我们继续我们的规则。现在我们将一个谜题转换成逻辑。
Blue: You are in the parlor
White: This box is empty
Black: The blue box is true
这转化为：
constBlueStatement = True;
constWhiteStatement = Not(WhiteBoxHasGems);
constBlackStatement = BlueBoxIsTrue;
现在我们继续制定更多的规则。首先，我们将编写一个助手。Equiv意味着两个表达式是等效的，它们必须都为真或都为假：
constEquiv = (p, q) => Or(
And(p, q),
And(Not(p), Not(q)),
);
现在，一个盒子为“真”意味着它的所有陈述都为真，而一个盒子为“假”意味着它的所有陈述都为假。
constBlueTruth = And(
Equiv(BlueBoxIsTrue, BlueStatement),
Equiv(BlueBoxIsFalse, Not(BlueStatement)),
);
constWhiteTruth = And(
Equiv(WhiteBoxIsTrue, WhiteStatement),
Equiv(WhiteBoxIsFalse, Not(WhiteStatement)),
);
constBlackTruth = And(
Equiv(BlackBoxIsTrue, BlackStatement),
Equiv(BlackBoxIsFalse, Not(BlackStatement)),
);
constStatementTruths = And(
BlueTruth,
WhiteTruth,
BlackTruth,
);
此实现假定每个框仅发出一个语句，我们可以稍后修复，现在不用担心。
现在我们的StatementTruths表达式看起来像这样：
(((BlueBoxIsTrue ∧ T) ∨ (¬BlueBoxIsTrue ∧ F)) ∧ ((BlueBoxIsFalse ∧ F) ∨ (¬BlueBoxIsFalse ∧ T)))
∧ (((WhiteBoxIsTrue ∧ ¬WhiteBoxHasGems) ∨ (¬WhiteBoxIsTrue ∧ WhiteBoxHasGems)) ∧ ((WhiteBoxIsFalse ∧ WhiteBoxHasGems) ∨ (¬WhiteBoxIsFalse ∧ ¬WhiteBoxHasGems)))
∧ (((BlackBoxIsTrue ∧ BlueBoxIsTrue) ∨ (¬BlackBoxIsTrue ∧ ¬BlueBoxIsTrue)) ∧ ((BlackBoxIsFalse ∧ ¬BlueBoxIsTrue) ∨ (¬BlackBoxIsFalse ∧ BlueBoxIsTrue)))
哎呀，有点丑，其实。看，我们有一个与True进行AND运算的表达式。这很好，但它在美学上冒犯了我。我们可以简化的东西。让我们对And构造函数进行一些修改。
constAnd = (...terms) => {
// And of zero things is true.
if (terms.length === 0) {
returnTrue;
}
// And of one thing is just that thing.
if (terms.length === 1) {
return terms[0];
}
for (let t of terms) {
// Any explicit Falses make the whole expression False.
if (t.type === 'false') {
returnFalse;
}
// Any explicit Trues can just be excluded, they don't affect the result.
if (t.type === 'true') {
let newTerms = [];
for (let t of terms) {
if (t.type !== 'true') {
newTerms.push(t);
}
}
returnAnd(...newTerms);
}
}
// If any of the terms are Ands already, flatten them.
for (let t of terms) {
if (t.type === 'and') {
let newTerms = [];
for (let t of terms) {
if (t.type === 'and') {
newTerms.push(...t.terms);
} else {
newTerms.push(t);
}
}
returnAnd(...newTerms);
}
}
return {
type: 'and',
terms,
};
};
我们可以对Or和Not进行一些类似的调整。请注意，我们不希望在这里过度使用重写，因为这样的重写可能需要指数级的时间。但是我们很乐意只清理一下。
现在StatementTruths看起来像这样：
BlueBoxIsTrue
∧ ¬BlueBoxIsFalse
∧ ((WhiteBoxIsTrue ∧ ¬WhiteBoxHasGems) ∨ (¬WhiteBoxIsTrue ∧ WhiteBoxHasGems))
∧ ((WhiteBoxIsFalse ∧ WhiteBoxHasGems) ∨ (¬WhiteBoxIsFalse ∧ ¬WhiteBoxHasGems))
∧ ((BlackBoxIsTrue ∧ BlueBoxIsTrue) ∨ (¬BlackBoxIsTrue ∧ ¬BlueBoxIsTrue))
∧ ((BlackBoxIsFalse ∧ ¬BlueBoxIsTrue) ∨ (¬BlackBoxIsFalse ∧ BlueBoxIsTrue))
好多了！
最后，我们的最终规则是：
constGameRules = And(
BaseRules,
StatementTruths,
);
这是
((BlueBoxHasGems∧¬WhiteBoxHasGems∧¬BlackBoxHasGems)∨(¬BlueBoxHasGems∧WhiteBoxHasGems∧¬BlackBoxHasGems)∨(¬BlueBoxHasGems∧¬WhiteBoxHasGems∧BlackBoxHasG
ems))
∧(BlueBoxIsTrue∨WhiteBoxIsTrue∨BlackBoxIsTrue)
∧(BlueBoxIsFalse∨WhiteBoxIsFalse∨BlackBoxIsFalse)
∧BlueBoxIsTrue
∧¬BlueBoxIsFalse
∧((WhiteBoxIsTrue∧¬WhiteBoxHasGems)∨(¬WhiteBoxIsTrue∧WhiteBoxHasGems))
∧((WhiteBoxIsFalse∧WhiteBoxHasGems)∨(¬WhiteBoxIsFalse∧¬WhiteBoxHasGems))
∧((BlackBoxIsTrue∧BlueBoxIsTrue)∨(¬BlackBoxIsTrue∧¬BlueBoxIsTrue))
∧((BlackBoxIsFalse∧¬BlueBoxIsTrue)∨(¬BlackBoxIsFalse∧BlueBoxIsTrue))
现在，游戏归结为：找到对变量的所有令人满意的赋值，并弄清楚它们对应于哪个奖品位置。如果他们都同意奖品位置，则谜题有效。如果他们不同意奖品位置，则谜题没有唯一的解决方案。
现在我们需要一种评估表达式的方法。我们将看到以我们所做的方式使我们的构造函数具有自简化的一个有趣的后果：我们可以简单地遍历我们的树，用它们的真或假替换变量，然后让简化清理所有内容。这有点奇怪：eval 的输出是另一个表达式，而不是一个值，但是由于我们为每个变量赋予了值，所以该表达式将始终只是一个文字真或假：
constEval = (term, bindings) => {
switch (term.type) {
case 'true':
case 'false':
return term;
case 'var':
if (bindings.hasOwnProperty(term.name)) {
if (bindings[term.name]) {
returnTrue;
} else {
returnFalse;
}
} else {
// No assignment given.
return term;
}
case 'and':
return And(
...term.terms.map(x => Eval(x, bindings)),
);
case 'or':
return Or(
...term.terms.map(x => Eval(x, bindings)),
);
case 'not':
return Not(Eval(term.term, bindings));
default:
throw new Error(`can't eval ${term.type}`);
}
};
const a = Var("a");
const b = Var("b");
console.log(
Write(Eval(And(a, b), {})),
Write(Eval(And(a, b), { a: true })),
Write(Eval(And(a, b), { b: true })),
Write(Eval(And(a, b), { a: true, b: true })),
Write(Eval(And(a, b), { b: false })),
)
这输出：
(a ∧ b) -> no variable assignments were given.
b -> `a` was true, so it got eliminated.
a -> `b` was true, so it got eliminated.
T -> both were true, so the whole expression simplified to True
F -> `b` was false, so the whole expression simplified to False.
现在我们可以编写一个小助手来枚举（指数级的）对一组变量的赋值：
function* assignments(...variables) {
let totalCount = 1 << variables.length;
for (let i = 0; i < totalCount; i++) {
let result = {};
for (let j = 0; j < variables.length; j++) {
result[variables[j].name] = (i & (1 << j)) !== 0;
}
yield result;
}
}
让我们尝试一下：
console.log([...assignments(Var("a"), Var("b"))]);
这将枚举对a和b的每个可能的赋值：
[
{ a: false, b: false },
{ a: true, b: false },
{ a: false, b: true },
{ a: true, b: true }
]
现在我们可以找到所有满足我们谜题的赋值：
for (let binding of assignments(
BlueBoxIsTrue,
WhiteBoxIsTrue,
BlackBoxIsTrue,
BlueBoxIsFalse,
WhiteBoxIsFalse,
BlackBoxIsFalse,
BlueBoxHasGems,
WhiteBoxHasGems,
BlackBoxHasGems,
)) {
let result = Eval(GameRules, binding);
if (result.type === 'true') {
console.log(binding);
}
}
只有一个输出：
{
BlueBoxIsTrue: true,
WhiteBoxIsTrue: false,
BlackBoxIsTrue: true,
BlueBoxIsFalse: false,
WhiteBoxIsFalse: true,
BlackBoxIsFalse: false,
BlueBoxHasGems: false,
WhiteBoxHasGems: true,
BlackBoxHasGems: false
}
这确实对应于白色盒子拥有宝石！
让我们尝试我们的具有多种解释的示例：
Blue: the gems are in a box with a true statement
White: the gems are in a box with a false statement
Black: The white box is true
这很容易转化为逻辑：
constBlueStatement = Or(
And(BlueBoxIsTrue, BlueBoxHasGems),
And(WhiteBoxIsTrue, WhiteBoxHasGems),
And(BlackBoxIsTrue, BlackBoxHasGems),
);
constWhiteStatement = Or(
And(BlueBoxIsFalse, BlueBoxHasGems),
And(WhiteBoxIsFalse, WhiteBoxHasGems),
And(BlackBoxIsFalse, BlackBoxHasGems),
);
constBlackStatement = WhiteBoxIsTrue;
现在有两个令人满意的赋值：
{
BlueBoxIsTrue: false,
WhiteBoxIsTrue: true,
BlackBoxIsTrue: true,
BlueBoxIsFalse: true,
WhiteBoxIsFalse: false,
BlackBoxIsFalse: false,
BlueBoxHasGems: true,
WhiteBoxHasGems: false,
BlackBoxHasGems: false
}
{
BlueBoxIsTrue: true,
WhiteBoxIsTrue: false,
BlackBoxIsTrue: false,
BlueBoxIsFalse: false,
WhiteBoxIsFalse: true,
BlackBoxIsFalse: true,
BlueBoxHasGems: true,
WhiteBoxHasGems: false,
BlackBoxHasGems: false
}
但正如我们所希望的，在它们两个中，蓝色盒子都拥有宝石。
我们可以在这里结束循环并自动化此过程：
let gemBoxes = new Set();
for (let binding of assignments(
BlueBoxIsTrue,
WhiteBoxIsTrue,
BlackBoxIsTrue,
BlueBoxIsFalse,
WhiteBoxIsFalse,
BlackBoxIsFalse,
BlueBoxHasGems,
WhiteBoxHasGems,
BlackBoxHasGems,
)) {
let result = Eval(GameRules, binding);
if (result.type === 'true') {
if (binding.BlueBoxHasGems) {
gemBoxes.add('blue');
}
if (binding.WhiteBoxHasGems) {
gemBoxes.add('white');
}
if (binding.BlackBoxHasGems) {
gemBoxes.add('black');
}
}
}
if (gemBoxes.size === 0) {
console.log("FAIL: no valid assignments");
} else if (gemBoxes.size === 1) {
console.log(`gems are in ${[...gemBoxes][0]} box`);
} else if (gemBoxes.size === 2) {
console.log("FAIL: multiple valid assignment");
}
就这样！这解决了问题的一半，实际上是在将英文文本翻译成逻辑后解决难题。下周我们将解决上半部分。
如果您想在本篇文章中弄乱代码，它可以以某种形式存在于此处。
不要错过接下来的内容。订阅 Justin Jaffray 的 NULL BITMAP： Your email (you@example.com) Subscribe Continue the conversation:
— Start the conversation: Comment and Subscribe GitHub Website Bluesky Twitter Find NULL BITMAP by Justin Jaffray elsewhere: GitHub Website Bluesky Twitter This email brought to you by Buttondown, the easiest way to start and grow your newsletter.