[Proof Complexity] MIAO seminar Monday Nov 21 at 14:00 CET with Kilian Risse: Bounded depth proof for Tseitin formulas on the grid; revisited

Jakob Nordström jakob.nordstrom at cs.lth.se
Fri Nov 4 19:16:30 CET 2022

Dear all,

On Monday November 21 at 14:00 we are happy to invite you to a seminar with Doctor Kilian Risse from KTH Royal Institute of Technology. Kilian will tell us about some of the latest news from the proof complexity frontier, which was included as one of the contributions in his PhD thesis and was also presented at FOCS yesterday. The seminar is titled "Bounded depth proof for Tseitin formulas on the grid; revisited" and you find the abstract at the bottom of this message.

We will run this as a hybrid seminar at the University of Copenhagen. Local participants are warmly welcome on UCPH campus --- the exact location will be communicated later. Other participants are equally warmly welcome to join virtually at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://www.youtube.com/channel/UCN0G2Wfl9-sAKrVLVza7z4A (where, incidentally, a number of seminar videos from earlier this autumn and summer have now finally been published) for people who would like to hear the talk but cannot attend.

Most of our seminars consist of two parts: first a 50-55-minute regular talk, and then after a break a ca-1-hour in-depth technical presentation with (hopefully) a lot of interaction. The intention is that the first part of the seminar will give all listeners a self-contained overview of some exciting research results, and after the break people who have the time and interest will get an opportunity to really get into the technical details. (However, for those who feel that the first part was enough, it is perfectly fine to just discretely drop out during the break. No questions asked; no excuses needed.)

More information about upcoming MIAO seminars can be found at http://www.jakobnordstrom.se/miao-seminars/ . In particular, don't miss the seminar with Thore Husfeldt this coming Monday November 7! If you do not wish to receive these announcements, or receive several copies of them, please send a message to jn at di.ku.dk.

Best regards,
Jakob Nordström


Monday Nov 21 at 14:00 in Copenhagen and on Zoom
Bounded depth proof for Tseitin formulas on the grid; revisited
(Kilian Risse, KTH Royal Institute of Technology)

In this seminar we are going to study the Frege proof system: a Frege refutation of a CNF formula F is a sequence of Boolean formulas, where each formula is either a clause from F or follows from two previously derived formulas according to some derivation rule. The final formula in the sequence should be the constant false formula so that if the derivation rules are sound, then we can conclude that F has no satisfying assignment. The length of a refutation is the number of formulas in the sequence, the depth is the maximum (logical) depth of any formula occurring and, similarly, the line-size is the maximum size of any formula in the sequence.

We consider Frege refutations restricted to depth d and line-size M of the Tseitin formula defined over the n × n grid 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.

The first hour includes a gentle introduction to the Frege proof system and covers the necessary background to prove our lower bounds. In the second hour we are going to start with a sketch of the single switching lemma and, if time permits, we then cover the proof of the multi-switching lemma.

Based on joint work with Johan Håstad. Preprint available at https://arxiv.org/abs/2209.05839 .

Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +46 70 742 21 98

More information about the Proof-Complexity mailing list