Abstract
We consider Frege refutations restricted to depth d and line-size M of the Tseitin formula defined over the n × n torus and show that such refutations are of length exponential in n / (log M)^O(d). This improves upon a recent result of [Pitassi et al. '21]. The key technical step is a multi-switching lemma extending the switching lemma of [Håstad '17] for a space of restrictions related to the Tseitin contradiction.
In this talk we cover the standard tools used to prove bound depth Frege lower bounds and outline the proof of our switching lemma.
Based on joint work with Johan Håstad.