Prefer a chat interface with context about you and your work?
On Bounded Depth Proofs for Tseitin Formulas on the Grid; Revisited
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. [12]. The …