On Small-Depth Frege Proofs for Tseitin for Grids
Johan Håstad · 2017
We prove a lower bound on the size of a small depth Frege refutation of the Tseitin contradiction on the grid. We conclude that polynomial size such refutations must use formulas of almost logarithmic depth.