关于网格上 Tseitin 公式的有界深度证明（再探）

我们研究在 $n \times n$ 网格上对 Tseitin 矛盾使用深度-$d$ 布尔公式的 Frege 证明。我们证明若证明中每一行的规模为 $M$，则行数为 $n/(\log M)^{O(d)}$ 的指数级。这加强了 Pitassi 等人 [PRT22] 近期的结果。关键技术步骤是一个多切换引理，它推广了 H\r{a}stad [H\r{a}s20] 针对与 Tseitin 矛盾相关的限制空间所提出的切换引理。这一加强的引理还使我们将有界深度 Frege 反驳的标准证明大小下界从 $\tilde \Omega (n^{1/59d})$ 的指数级提升到 $\tilde \Omega (n^{1/d})$ 的指数级。这加强了本文 preliminary 版本 [HR22] 中给出的界。