MIAO Talk by Kilian Risse

Abstract:

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.

MIAO seminars:

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/. If you do not wish to receive these announcements, or receive several copies of them, please send a message to jn@di.ku.dk.