On Bounded Depth Proofs For Tseitin Formulas On The Grid; Revisited
summary
Proves that bounded-depth Frege refutations of the Tseitin formula on an n × n torus require length exp( n / (log M)^O(d) ) when every line has size ≤ M and depth ≤ d, resolving a conjecture and improving prior exp(n^{1/(58d)}) bounds to exp(n^{1/(d−1)}) in some regimes. Key tool is a multi-switching lemma that extends Håstad’s switching lemma to the affine restrictions used on the n×n torus Tseitin instance, and the restriction construction yields the claimed exponential separations.
AI-written summary · about
chapters (12)
- 0:00Start
- 0:38Some Proof Systems
- 1:34Frege Proof System
- 5:25Tseitin Formula
- 6:31Pigeonhole Principle
- 6:57History
- 13:59Proof Outline: Bounded Depth Circuit Lower Bounds
- 15:40Applying the Switching Lemma
- 15:58Proof Outline: Bounded Depth Frege Lower Bounds
- 18:47Multi-Switching Lemma
- 20:48The Restriction p
- 25:17Conclusion and Open Problems
related talks
40mUtilizing Structure in Combinatorial Solving and Reasoning
52mNumbers, Logic, and Decidability for Cyber-Physical Systems
32mCombinatorial Proofs of Concentration Bounds
15mFormal Assurance for Railway Interlockings: Verifying Z3 SAT Proofs with Tseitin in Rocq
27mRooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separatio...
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs
24mA New Conjecture on Hardness of Low-Degree 2-CSP’s with...
21mMechanised Hypersafety Proofs about Structured Data