2.3 条件的可满足性
独立游戏的叙事设计与分支对话 里有这样一类经验：一个条件如果永远触发不了，玩家就永远看不到它背后的内容——那是从体验出发的担忧。本节把它变成可判定的：给定一份规格，能不能证明某个条件在任何状态下都不成立？能，而且不需要枚举整条路径。
这就是可满足性（satisfiability）。2.1 给了求值器（给定状态，返回真假），2.2 给了它的步数，本节问第三个问题：这个条件有没有可能为真。一个恒假的条件是死条件——它挂在选项上，那条选项永不出现；挂在结局上，那个结局永不可达。
有限状态域
判定在一个有限状态域里做：节点 14 个 × 好感度 4 个各 ∈ [0,100] 整数（101⁴）× flag 18 个布尔（2¹⁸）× 物品 9 个布尔（2⁹），全乘起来是 195534508357844992（约 1.96×10¹⁷）个状态。条件不读节点，所以可满足性只在「好感度 × flag × 物品」上判定——节点维度不参与。
判定：边界值枚举
直接枚举 10¹⁷ 个状态不可能，但这份文法有结构可乘：每个被引用的变量彼此独立，而一个原子谓词（flag 名 == 0|1、item 名 == 0|1、aff 名 op n）的真值只依赖那一个变量。于是：
- 被引用的
flag/item名字取{0,1}；不在状态域里的名字固定取默认 0。 - 被引用的好感度名字取其全部阈值的边界值
{n−1, n, n+1}并上{0,100}；域外名字固定取默认 0。
对这些比较算子，一个变量的真值向量在每个阈值区间内是常数，所以边界值集合覆盖了全部可区分的真值向量——枚举是完备的：既不误报，也不像区间过近似那样漏报。被引用的变量通常只有一两个，枚举量因此很小。
恒假 = 死条件。按成因分两类：dead_threshold（名字在域内，但组合自相矛盾）与 dead_structural（引用了域外名字，永远取默认 0）。
S 层：可满足性扫描
#!/usr/bin/env python3
# file: sim/ne_02_3_satisfiability.py
# tier: S
# verify: /opt/homebrew/bin/python3 sim/ne_02_3_satisfiability.py
"""卷二 2.3 条件的可满足性（S 层）：在有限状态域里判定一个条件是否可被满足。
状态域 = 节点 × 4 个好感度 ∈ [0,100] × 18 个 flag ∈ {0,1} × 9 个物品 ∈ {0,1}。
条件不读节点，故可满足性只在 (好感度 × flag × 物品) 上判定。判定用**边界值枚举**：
被引用的 flag/item 取 {0,1}（域外名字固定取默认 0），被引用的好感度取其全部阈值
{n-1, n, n+1} ∪ {0,100}（域外名字固定取默认 0）——对这些比较算子，边界值覆盖了全部
可区分的真值向量，故枚举**完备**：既不误报，也不像区间过近似那样漏报。
恒假 = 死条件。区分两类成因：
dead_structural —— 条件引用的名字不在状态域里（如 lin / hai 声明了 affinity 却不在
state.vars），求值时永远取默认 0，门限结构性不可达。
dead_threshold —— 名字在域内，但组合自相矛盾（如 and 里一个 >=30 一个 <30）。
复用 sim/na_00_spec_check.py 的 load_spec。产出 out/ne_02_3_satisfiability.json。
"""
from __future__ import annotations
import itertools
import json
import os
import sys
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)
import na_00_spec_check as base # noqa: E402 复用 load_spec 与 eval_cond
OUT = os.path.join(os.path.dirname(HERE), "out/ne_02_3_satisfiability.json")
def sites(spec: dict) -> list:
out = []
for n in spec["dialogue"]:
if n.get("line_when"):
out.append(("line_when", f"{n['id']}.line_when", n["line_when"]))
for c in (n.get("choices") or []):
if c.get("when"):
out.append(("choice", f"{n['id']}/{c['id']}", c["when"]))
for e in spec["scene_graph"]["edges"]:
if e.get("when"):
out.append(("edge", f"{e['from']}->{e['to']}", e["when"]))
for nd in spec["scene_graph"]["nodes"]:
if nd.get("enter_when"):
out.append(("enter_when", f"node {nd['id']}", nd["enter_when"]))
for loc in spec["world"]["locations"]:
if loc.get("unlock_when"):
out.append(("unlock_when", f"location {loc['id']}", loc["unlock_when"]))
for e in spec["endings"]:
if e.get("when"):
out.append(("ending", f"ending {e['id']}", e["when"]))
return out
def collect(c, fnames: set, inames: set, affs: dict) -> None:
"""递归收集条件树引用的名字与好感度阈值。"""
if c is None:
return
k = c[0]
if k == "flag":
fnames.add(c[1])
elif k == "item":
inames.add(c[1])
elif k == "aff":
affs.setdefault(c[1], set()).add(c[3])
elif k in ("and", "or"):
collect(c[1], fnames, inames, affs)
collect(c[2], fnames, inames, affs)
elif k == "not":
collect(c[1], fnames, inames, affs)
def satisfiable(c, df: set, di: set, dv: set) -> tuple:
"""(是否可满足, 是否引用域外名字)。边界值枚举，完备。"""
fnames, inames, affs = set(), set(), {}
collect(c, fnames, inames, affs)
out_of_domain = bool((fnames - df) | (inames - di) | (set(affs) - dv))
f_choices = [[(n, v) for v in ([0, 1] if n in df else [0])] for n in sorted(fnames)]
i_choices = [[(n, v) for v in ([0, 1] if n in di else [0])] for n in sorted(inames)]
a_choices = []
for n in sorted(affs):
if n not in dv:
a_choices.append([(n, 0)])
continue
cands = {0, 100}
for t in affs[n]:
for d in (-1, 0, 1):
if 0 <= t + d <= 100:
cands.add(t + d)
a_choices.append([(n, v) for v in sorted(cands)])
for fc in (itertools.product(*f_choices) if f_choices else [()]):
for ic in (itertools.product(*i_choices) if i_choices else [()]):
for ac in (itertools.product(*a_choices) if a_choices else [()]):
st = {"flags": dict(fc), "items": dict(ic), "aff": dict(ac)}
if base.eval_cond(c, st):
return True, out_of_domain
return False, out_of_domain
def main() -> int:
spec = base.load_spec()
df = set(spec["state"]["flags"])
di = set(spec["state"]["items"])
dv = set(spec["state"]["vars"])
nodes = len(spec["scene_graph"]["nodes"])
domain = nodes * (101 ** len(dv)) * (2 ** len(df)) * (2 ** len(di))
all_sites = sites(spec)
by_src, dead = {}, []
for src, key, c in all_sites:
by_src[src] = by_src.get(src, 0) + 1
ok, ood = satisfiable(c, df, di, dv)
if not ok:
dead.append({"src": src, "at": key, "cond": c,
"cause": "dead_structural" if ood else "dead_threshold"})
print(f"状态域规模：节点 {nodes} × 好感度 101^{len(dv)} × flag 2^{len(df)} × 物品 2^{len(di)} = {domain}")
print(f"条件位点 {len(all_sites)} 个：" + " / ".join(f"{k} {v}" for k, v in sorted(by_src.items())))
print(f"死条件（恒假）{len(dead)} 个：{[d['at'] for d in dead]}")
# 结构性不可达演示：lin / hai 声明了 affinity 却不在 state.vars
declared_chars = {c["id"] for c in spec["characters"]}
ghost = sorted(declared_chars - dv)
print(f"声明了 affinity 但不在 state.vars 的角色：{ghost}")
demo = ["aff", "lin", ">=", 30]
ok, ood = satisfiable(demo, df, di, dv)
print(f"演示条件 {demo}：可满足={ok} 引用域外名字={ood}（→ 结构性不可达）")
# 域内自相矛盾的演示
contra = ["and", ["aff", "yan", ">=", 60], ["aff", "yan", "<", 30]]
ok2, _ = satisfiable(contra, df, di, dv)
print(f"演示条件 {contra}：可满足={ok2}（→ 数值型死条件）")
report = {"domain": domain, "sites": len(all_sites), "by_source": by_src,
"dead": dead, "ghost_affinity": ghost,
"demo_structural_sat": ok, "demo_contradiction_sat": ok2}
os.makedirs(os.path.dirname(OUT), exist_ok=True)
with open(OUT, "w", encoding="utf-8") as fh:
json.dump(report, fh, ensure_ascii=False, indent=2)
fh.write("\n")
if dead:
print(f"FAIL 死条件 {len(dead)} 个：{[d['at'] for d in dead]}")
return 1
print("OK ne_02_3_satisfiability：全部条件位点在状态域内均可满足")
return 0
if __name__ == "__main__":
sys.exit(main())
本机实跑 /opt/homebrew/bin/python3 sim/ne_02_3_satisfiability.py：
状态域规模：节点 14 × 好感度 101^4 × flag 2^18 × 物品 2^9 = 195534508357844992
条件位点 57 个：choice 34 / edge 5 / ending 4 / enter_when 5 / line_when 2 / unlock_when 7
死条件（恒假）0 个：[]
声明了 affinity 但不在 state.vars 的角色：['hai', 'lin']
演示条件 ['aff', 'lin', '>=', 30]：可满足=False 引用域外名字=True（→ 结构性不可达）
演示条件 ['and', ['aff', 'yan', '>=', 60], ['aff', 'yan', '<', 30]]：可满足=False（→ 数值型死条件）
OK ne_02_3_satisfiability：全部条件位点在状态域内均可满足
P 层：判定器的正负例
P 层重写同一判定器，对真实规格断言 0 死条件，再用注入负例证明它会开火：
// file: core/src/inkwell/ne_02_3_satisfiability.ts
// tier: P
// verify: node --test 'core/test/ne_02_3_satisfiability.test.ts'
// 卷二 2.3：条件可满足性判定。在有限状态域（好感度 ∈ [0,100] × flag ∈ {0,1} × 物品 ∈ {0,1}）
// 上判定一个条件是否可被满足。用边界值枚举：被引用的好感度取全部阈值 {n-1,n,n+1} ∪ {0,100}，
// flag/item 取 {0,1}；域外名字固定取默认 0。对这些比较算子，枚举完备——不误报也不漏报。
import { condOk } from "./engine.ts";
import type { Cond, State } from "./engine.ts";
function mkState(flags: Record<string, number>, items: Record<string, number>, aff: Record<string, number>): State {
return { node: "x", aff, flags, items, path: [] };
}
function collect(
c: Cond | null | undefined,
fnames: Set<string>,
inames: Set<string>,
affs: Map<string, Set<number>>,
): void {
if (!c) return;
const k = c[0] as string;
if (k === "flag") fnames.add(c[1] as string);
else if (k === "item") inames.add(c[1] as string);
else if (k === "aff") {
const n = c[1] as string;
if (!affs.has(n)) affs.set(n, new Set<number>());
affs.get(n)!.add(c[3] as number);
} else if (k === "and" || k === "or") {
collect(c[1] as Cond, fnames, inames, affs);
collect(c[2] as Cond, fnames, inames, affs);
} else if (k === "not") {
collect(c[1] as Cond, fnames, inames, affs);
}
}
function prod(arrs: [string, number][][]): Record<string, number>[] {
let acc: [string, number][][] = [[]];
for (const opts of arrs) {
const next: [string, number][][] = [];
for (const base of acc) for (const o of opts) next.push([...base, o]);
acc = next;
}
return acc.map((pairs) => Object.fromEntries(pairs) as Record<string, number>);
}
/** (是否可满足, 是否引用了域外名字)。 */
export function satisfiable(
c: Cond,
df: Set<string>,
di: Set<string>,
dv: Set<string>,
): { sat: boolean; outOfDomain: boolean } {
const fnames = new Set<string>();
const inames = new Set<string>();
const affs = new Map<string, Set<number>>();
collect(c, fnames, inames, affs);
const outOfDomain =
[...fnames].some((n) => !df.has(n)) ||
[...inames].some((n) => !di.has(n)) ||
[...affs.keys()].some((n) => !dv.has(n));
const fVals = [...fnames].sort().map((n) => (df.has(n) ? [0, 1] : [0]).map((v) => [n, v] as [string, number]));
const iVals = [...inames].sort().map((n) => (di.has(n) ? [0, 1] : [0]).map((v) => [n, v] as [string, number]));
const aVals = [...affs.keys()].sort().map((n) => {
if (!dv.has(n)) return [[n, 0] as [string, number]];
const cands = new Set<number>([0, 100]);
for (const t of affs.get(n)!) for (const d of [-1, 0, 1]) if (t + d >= 0 && t + d <= 100) cands.add(t + d);
return [...cands].sort((a, b) => a - b).map((v) => [n, v] as [string, number]);
});
for (const flags of prod(fVals)) {
for (const items of prod(iVals)) {
for (const aff of prod(aVals)) {
if (condOk(c, mkState(flags, items, aff))) return { sat: true, outOfDomain };
}
}
}
return { sat: false, outOfDomain };
}
本机实跑 node --test 'core/test/ne_02_3_satisfiability.test.ts'：
可满足性：57 个条件位点，死条件 0 个
✔ 真实规格：57 个条件位点无一为恒假（死条件 0 个） (1.539333ms)
✔ 边界：yan >= 100 在状态域内可满足（域口径不同于可达口径） (0.096791ms)
✔ 负例一 · 结构性不可达：lin 不在 state.vars，任何门限恒假 (0.077084ms)
✔ 负例二 · 数值型自相矛盾：yan >= 60 且 yan < 30 恒假 (0.08525ms)
✔ 负例三 · 重言式可满足：flag 与 not flag 的析取恒真 (0.067125ms)
✔ 负例四 · 域外 flag：从未声明的 flag 恒假 (0.057542ms)
ℹ tests 6
ℹ suites 0
ℹ pass 6
ℹ fail 0
ℹ cancelled 0
ℹ skipped 0
ℹ todo 0
ℹ duration_ms 248.37925
判读：0 个死条件，以及一个口径问题
第一，本规格 0 个死条件。 57 个条件位点（34 个带条件选项 + 5 条带条件场景边 + 4 个带条件结局 + 5 个节点 enter_when + 7 个地点 unlock_when + 2 个 line_when）在状态域里全部可满足。5 个结局里 e_dark 的 when 是 null（无条件），所以带条件的结局是 4 个而非 5 个——null 不算条件，它恒真。
第二，域口径与可达口径是两回事。 本节判的是「在状态域里有没有解」，卷一 13.2 语义校验：可满足性与死条件
判的是「在可达状态里有没有解」。["aff","yan",">=",100] 在域口径下可满足（把 yan 设成 100 即可），在可达口径下却可能不可达（沿所有路径 yan 到不了 100）。前者是结构性质，后者是可达性质；两者都会抓到死条件，但结论可以不同。本节用域口径，因为它是精确的（边界值枚举完备），而可达口径只能过近似。
第三，lin / hai 那处真实特征。 规格里 lin 与 hai 两个角色声明了 affinity（{"init":40,...} / {"init":60,...}），却不在 state.vars 里、也从未被任何选项 add 过。于是求值器对它们的取值永远是默认 0——任何对 lin / hai 的门限都结构性不可达。演示条件 ["aff","lin",">=",30] 被判为不可满足，且 引用域外名字=True。
这算不算「死条件」，取决于口径，要写清：
| 口径 | 判定 | 成因分类 | 修法 |
|---|---|---|---|
| 域口径（本节） | 恒假，判死 | dead_structural | 要么把 lin 补进 state.vars，要么删掉该条件 |
| 可达口径（卷一 13.2） | 不可达，判死 | 区间缺失 | 同上 |
两种口径都判它「不可达」，但成因与修法和 dead_threshold（如把阈值抬到区间外）不同，所以本节把两类分开报。要点在于：本规格里实测 0 个条件引用了 lin / hai——所以这是一处潜在风险而非现存缺陷。分析器把域外名字标出来，是为了防止将来有人写下 ["aff","lin",">=",30] 却没人发现：条件永远为假，那条选项永远不出现，而规格文本看起来完全正常。
自检表
| 检查项 | 合格标准 |
|---|---|
| 判定完备 | 边界值覆盖全部可区分真值向量，不误报也不漏报 |
| 域外名字可识别 | 引用不在状态域里的名字，标 dead_structural |
| 两类成因分开 | dead_structural 与 dead_threshold 分列，修法不同 |
| 口径写明 | 明确是「域口径」，与可达口径区分 |
| 负例证明会开火 | 恒假、重言式、域外名字各配一个注入用例 |
求值器（2.1）、它的步数（2.2）、它的可满足性（2.3）——本节把「条件」这条线走完。下一个问题是：条件成立之后，选项带来的效果怎么作用到状态上，以及为什么推进必须确定，而 set 类幂等与 add 类累加需要分别验证。那是下一章。
阅读导航：上一节：2.2 短路与复杂度 · 下一节：3.1 效果的应用 。
继续阅读
探索更多技术文章
浏览归档，发现更多关于系统设计、工具链和工程实践的内容。