[Proof Complexity] MIAO seminar Tue Mar 4 at 14:00 CET with Duri Andrea Janett: Truly supercritical trade-offs for resolution, cutting planes, monotone circuits, and Weisfeiler–Leman

[Jakob Nordström]

Dear all,

On Tuesday March 4 at 14:00 CET we will have the opportunity to listen 
to the MIAO seminar "Truly supercritical trade-offs for resolution, 
cutting planes, monotone circuits, and Weisfeiler–Leman" given by our 
very own Duri Andrea Janett. 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 to Auditorium No. 8 in the Hans 
Christian Ørsted Building at Universitetsparken 5, while 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://youtube.com/@MIAOresearch 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 the MIAO seminar series can be found at 
https://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 at di.ku.dk.

Best regards,
Jakob Nordström

**********

/Tuesday Mar 4 at 14:00 in Auditorium No. 8, Hans Christian Ørsted 
Building, Universitetsparken 5, University of Copenhagen, and on Zoom
*Truly supercritical trade-offs for resolution, cutting planes, monotone 
circuits, and Weisfeiler–Leman
*(Duri Andrea Janett, University of Copenhagen and Lund University)
/
We exhibit supercritical trade-off for monotone circuits, showing that 
there are functions computable by small circuits for which any circuit 
must have depth super-linear or even super-polynomial in the number of 
variables, far exceeding the linear worst-case upper bound. We obtain 
similar trade-offs in proof complexity, where we establish the first 
size-depth trade-offs for cutting planes and resolution that are truly 
supercritical, i.e., in terms of formula size rather than number of 
variables, and we also show supercritical trade-offs between width and 
size for treelike resolution.

Our results build on a new supercritical depth-width trade-off for 
resolution, obtained by refining and strengthening the compression 
scheme for the cop-robber game in [Grohe, Lichter, Neuen & Schweitzer 
2023]. This yields robust supercritical trade-offs for dimension versus 
iteration number in the Weisfeiler–Leman algorithm. Our other results 
follow from improved lifting theorems that might be of independent interest.

In the second (blackboard) part of the talk, we will focus on the proof 
of the depth-width trade-off. In particular, we will describe a strategy 
for the robber in the compressed cop-robber game, which corresponds to 
the depth lower bound in the small-width regime.

This is joint work with Susanna F. de Rezende, Noah Fleming, Jakob 
Nordström, and Shuo Pang to appear at /STOC '25./


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se