On Bounded Depth Proofs For Tseitin Formulas On The Grid; Revisited

Channel:
United States Simons Institute for the Theory of Computing
Subscribers:
68,700
Published on ● Video Link: https://www.youtube.com/watch?v=9g4y5TgCLyI


Duration: 30:16
129 views
6

Kilian Risse (Ecole Polytechnique Fédérale de Lausanne (EPFL))
https://simons.berkeley.edu/talks/kilian-risse-ecole-polytechnique-federale-de-lausanne-epfl-2023-04-17
Satisfiability: Theory, Practice, and Beyond

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.



Other Videos By Simons Institute for the Theory of Computing


2023-04-19Theoretical limits of 1UIP Learning
2023-04-19The Proof Complexity of Integer Programming
2023-04-19The Power of Unentangled Quantum Proofs With Non-negative Amplitudes | Quantum Colloquium
2023-04-19Beyond SAT - Proofs for QBF, and more
2023-04-19Isomorph-Free Generation Of Combinatorial Objects With Sat Modulo Symmetries
2023-04-18A Roadmap for the Next Phase of SAT Research
2023-04-18Structure-guided Local Improvement for Maximum Satisfiability
2023-04-18Designing Samplers is Easy: The Boon of Testers
2023-04-18IPASIR-UP: User Propagators for CDCL
2023-04-18CDCL SAT Solving and Applications to Optimization Problems
2023-04-18On Bounded Depth Proofs For Tseitin Formulas On The Grid; Revisited
2023-04-18A Survey of Automatability
2023-04-17In Search of the Hard Instances
2023-04-12Gödel and the Vicious Circle: On the (In)Feasibility of Lower Bounds
2023-04-12Quantum Pseudoentanglement | Quantum Colloquium
2023-04-05Building Human Intelligence at Scale, to Save the Next Generation from ChatGPT
2023-03-30A Theory of ToniCS
2023-03-30Randomized versus Deterministic Decision Tree Size
2023-03-30Weak Automat*ability
2023-03-29Inspiration
2023-03-29Alvy Ray Smith | Polylogues


Tags:
Simons Institute
theoretical computer science
UC Berkeley
Computer Science
Theory of Computation
Theory of Computing
Satisfiability: Theory Practice and Beyond
Kilian Risse