On bounded depth proofs for Tseitin formulas on the grid; revisited

TL;DR

This paper establishes stronger lower bounds on the size of bounded depth Frege proofs for Tseitin formulas on grids, using advanced switching lemmas to improve previous exponential size bounds.

Contribution

It introduces a multi-switching lemma extending H {a}stad's lemma, leading to improved lower bounds for bounded depth Frege proof sizes for Tseitin contradictions.

Findings

Proof size lower bound improved from exponential in n^{1/59d} to exponential in n^{1/d}

Multi-switching lemma extends H {a}stad's switching lemma for Tseitin formulas

Strengthens previous bounds on bounded depth Frege proofs for grid Tseitin contradictions

Abstract

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\r{a}stad [H\r{a}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 \Omega (n^{1/59d})$ to exponential in $\tilde \Omega (n^{1/d})$. This strengthens the bounds given in the preliminary version of this paper [HR22].