公式规模博弈

玩家 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\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让一方持有真输入、另一方持有假输入并寻找分歧坐标的通信搜索关系。，而不是把这里的整数预算解释成消息长度。