公式规模博弈

玩家 I 像是在自顶向下设计一棵公式，却不能把预算同时花在所有分支后再挑容易的一支。他先声明根是 OR 还是 AND，并把总叶数拆成两份；玩家 II 总选择更难分开的那一侧，迫使 I 的方案对整组正反例都有效。若任何分支最终无法用一个文字收尾，就说明对应预算不够。这样，“排除所有小公式”被变成一个对抗式不变量：II 只需保证每次分割后至少有一支仍然混杂。

这里的状态保存的是两组赋值，而不是一对私有输入。集合让一次动作同时追踪许多可能的反例，因此适合叶数下界：每个叶只能用一个文字切开一部分正反例，AND/OR 结点只是把这些工作分配到子树。它与Karchmer–Wigderson 博弈理路Karchmer–Wigderson 博弈Karchmer-Wigderson game · KW game · Karchmer-Wigderson relation让一方持有真输入、另一方持有假输入并寻找分歧坐标的通信搜索关系。都反映公式语法，但前者分配叶预算、后者在单个输入对上计算最坏通信位数，玩家信息和资源量都不同。

令 $S=\{10,01,11\}$、$R=\{00\}$，目标函数是 $x_1\vee x_2$。在 $E{F}_2(S,R)$ 中，I 取 $u=v=1$，作左分割

若 II 选 $(1,C,R)$，文字 $x_1$ 分开两侧；若选 $(1,D,R)$，文字 $x_2$ 分开两侧。因此 I 必胜，恢复二叶公式 $x_1\vee x_2$。赋值 $11$ 同时属于 $C,D$ 并非重复记账错误：两个析取支式确实都在该输入上为真，而每条实际对局只由 II 选一支继续。反过来，在 $E{F}_1(S,R)$ 中，$x_1$ 不能分开 $01$ 与 $00$，$x_2$ 不能分开 $10$ 与 $00$，负文字也不行，所以 II 必胜，证明确需至少两个叶。

博弈刻画的是文字叶出现次数。二元公式的内部门数是叶数减一，规范语法的总符号数也与叶数同阶；深度却可能从对数级到线性级，不能说这些资源都只差常数因子。常量叶的约定同样影响精确等式：若 $S=\{0,1{\}}^n,R=\varnothing$，没有单个文字能在全部 $S$ 上为真，本页最小规模是 $x_1\vee \mathrm{\neg }{x}_1$ 的两个叶。若另允许常量 $1$ 作一个叶，就必须给博弈增加对应的常量终局；否则一叶公式与博弈不再吻合。若 $S\cap R\ne \varnothing$，任何公式都无法分开，同一个赋值会同时被要求接受和拒绝；博弈也相应由 II 获胜。对部分函数，只把承诺域内的 $1$ 输入放入 $S$、$0$ 输入放入 $R$，结论刻画的是承诺上的最小公式，不能自动推广到域外。

要证 $L(f)>w$，可取 $S=f^{-1}(1)$、$R=f^{-1}(0)$，为玩家 II 构造在 $E{F}_w(S,R)$ 中保持混杂的策略。更灵活时也可选较小的正反例子集；若这对子集已无法由 $w$ 个叶分开，完整函数当然更不可能。Hella–Väänänen 用该框架重述 Krapchenko 对 parity 的二次公式下界，其核心是统计相邻正负赋值之间必须由叶覆盖的边，而不是枚举所有公式。

这套集合分割语义可扩展到一阶、模态等逻辑：为量词或模态增加相应动作，同时让预算记录所选语法尺度。但扩展后的“公式大小”可能计量原子式、量词或联结词，不能把新规则倒灌回本页的命题叶规模。若目标是公式深度或最坏通信位数，应改用KW 搜索关系理路Karchmer–Wigderson 博弈Karchmer-Wigderson game · KW game · Karchmer-Wigderson relation让一方持有真输入、另一方持有假输入并寻找分歧坐标的通信搜索关系。，而不是把这里的整数预算解释成消息长度。