[Proof Complexity] MIAO seminar Mon Oct 20 at 14:00 CE(S)T with Sreejata Kishor Bhattacharya and Arkadev Chattopadhyay: Exponential lower bounds on the size of ResLin proofs of nearly quadratic depth

[Jakob Nordström]

Dear all,

On Monday October 20 at 14:00 CE(S)T, we will have the opportunity to listen to Sreejata Kishor Bhattacharya and Arkadev Chattopadhyay from the  Tata Institute of Fundamental Research Mumbai, who will present a seminar titled  "Exponential lower bounds on the size of ResLin proofs of nearly quadratic depth". You find the abstract at the bottom of this message.

This will be a video seminar 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.

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

**********

/Monday Oct 20 at 14:00 on Zoom
*Exponential lower bounds on the size of ResLin proofs of nearly quadratic depth
*(Sreejata Kishor Bhattacharya and Arkadev Chattopadhyay, Tata Institute of Fundamental Research Mumbai)
/
Itsykson and Sokolov (2014) identified resolution over parities, that we call ResLin, as a natural and simple fragment of AC0[2]-Frege for which no super-polynomial lower bounds on size of proofs are known. Building on a recent line of work, Efremenko and Itsykson (2025) proved lower bounds of the form exp(N^(Omega(1)), on the size of ResLin proofs whose depth is upper bounded by O(N log N), where N is the number of variables of the unsatisfiable CNF formula. The hard formula they used was Tseitin on an appropriately expanding graph, lifted by a 2-stifling gadget. They posed the natural problem of proving super-polynomial lower bounds on the size of proofs that are N^{1+eps} deep, for any constant eps > 0.

We provide a significant improvement by proving a lower bound on size of the form exp( Omega(N^eps),  as long as the depth of the ResLin proofs are O(N^{2-eps}) for  every eps > 0. Our hard formula is again Tseitin on an expander graph, albeit lifted with a different type of gadget. Our gadget needs to have small correlation with all parities.

An important ingredient in our work is to show that arbitrary distributions lifted with such gadgets fool "safe" affine spaces, an idea which originates in the earlier work of Bhattacharya, Chattopadhyay and Dvorak (2024).


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