论文标题
在网格上的三曲蛋白公式的有界深度证明上；重新审视
On bounded depth proofs for Tseitin formulas on the grid; revisited
论文作者
论文摘要
我们使用深度-D $ boolean公式在$ n \ times n $网格上研究弗雷格证明。我们证明，如果证明中的每一行是$ m $的，则行数为$ n/（\ log m）^{o（d）} $的指数为指数。这加强了Pitassi等人的最新结果。 [PRT22]。关键的技术步骤是一个多旋转引理，扩展了Håstad[hås20]的开关引理，以实现与三替蛋白矛盾有关的限制空间。加强的引理还使我们能够改善限制性深度驳斥的标准证明大小的下限，从$ \tildeΩ（n^{1/59d}）$中的指数替代，以$ \tildeΩ（n^{1/d}）$中的指数为指数。这加强了本文初步版本中给出的界限[HR22]。
We study Frege proofs using depth-$d$ Boolean formulas for the Tseitin contradiction on $n \times n$ grids. We prove that if each line in the proof is of size $M$ then the number of lines is exponential in $n/(\log M)^{O(d)}$. This strengthens a recent result of Pitassi et al. [PRT22]. The key technical step is a multi-switching lemma extending the switching lemma of Håstad [Hås20] for a space of restrictions related to the Tseitin contradiction. The strengthened lemma also allows us to improve the lower bound for standard proof size of bounded depth Frege refutations from exponential in $\tilde Ω(n^{1/59d})$ to exponential in $\tilde Ω(n^{1/d})$. This strengthens the bounds given in the preliminary version of this paper [HR22].
