Karchmer–Wigderson 博弈

一个真输入和一个假输入不可能在每一位都相同；困难不在分歧是否存在，而在双方各自只看见一半信息时怎样定位它。公式的每一层恰好替一方提供一次局部选择：OR 为真时，真输入持有者知道至少一个真孩子；AND 为假时，假输入持有者知道至少一个假孩子。通信路径因而逐层缩小到一个文字，最长 transcript 就是根到叶最长路径。

这个翻译把语法深度变成一个语义搜索问题。证明公式深度下界时，不必枚举所有树形表达式；只要证明任何协议都必须交换很多 bit。反过来，一个巧妙协议会机械地给出浅公式。这里精确刻画的是公式而非一般 DAG 电路：协议树的不同 transcript 不能共享后续子协议，正对应树中没有 fan-out。

取 $f(x)=x_1\vee x_2\vee x_3\vee x_4$。Bob 的假输入只能是 $0000$；Alice 收到例如 $x=0101$。按平衡 OR 公式，Alice 先发送一 bit 表示选择前半 $(x_1,x_2)$，再发送一 bit 选择其中的 $x_2$，输出坐标 $2$。若约定总挑最小的为真坐标，这对所有真输入形成深度 $2$ 的确定协议；其四个可能输出叶对应平衡四叶 OR 公式。一般 $O{R}_n$ 的成本为 $\lceil {\log }_{2}n\rceil$，与最小二元 OR 树深度一致。

对单调 $f$，单调 KW 关系要求输出 $x_i=1,y_i=0$ 的坐标。若不存在，则逐坐标有 $x\le y$，单调性会推出 $f(x)\le f(y)$，与 $1>0$ 矛盾。这个版本刻画单调公式深度；单调公式是单调电路公理库单调布尔电路Monotone circuit · Monotone Boolean circuit只用正输入、AND 与 OR 门计算单调布尔函数的无环电路模型。中 fan-out 为 $1$ 的特例。对非单调函数不能要求固定方向的 $1\to 0$ 分歧，例如 parity 的真、假输入可能只在 $0\to 1$ 方向不同。

KW 是关系问题而非双方共同计算一个单值函数；输出任一合法坐标即可。二元公式中选择孩子只需发送一 bit，因此通信位数与门深度逐层一致；若直接允许 $r$ 扇入门，一次选择可能需要 $\lceil {\log }_{2}r\rceil$ bit，精确等式必须随深度 convention 调整。随机协议、量子协议、允许错误的协议各对应不同资源，不能无条件替代上面的确定性精确等式。协议树的叶数也能联系公式规模，但本页的资源是通信深度；以正反例集合和显式叶预算为状态的公式规模博弈公理库公式规模博弈Formula-size game · Propositional formula-size game · EF_w formula game以正反例集合的左右分割和叶预算精确刻画命题公式的最小叶规模。是另一套刻画，不能把两页合并成同义定义。

单调 KW 博弈最初用于证明 $s$-$t$ 连通性的单调公式需要超对数深度：通信者必须从一张连通图和一张不连通图中找出方向正确的分歧边，图的割结构使搜索无法在太少轮中完成。该结论针对单调公式深度，不是一般连通性电路下界；允许否定或 DAG 共享会改变模型。

在 NC¹ 研究中，KW 视角把公式深度下界、协议组合与函数复合放到同一语言。若能证明复合函数的 KW 通信复杂度近似相加，就会得到更强公式下界，这也是 Karchmer–Raz–Wigderson 复合猜想一类问题的动机。它们仍是开放研究路线，不能写成已经给出超多项式一般电路下界的定理。