Proof complexity as a computational lens lecture 12: Tightness of size-width/degree relations

Thursday Dec 4, 2025
Proof complexity as a computational lens
Lecture 12: Tightness of size-width/degree relations for resolution and polynomial calculus
(Jakob Nordström, University of Copenhagen and Lund University)

In this lecture, we show that the lower bounds on size in terms of width/degree in [Ben-Sasson and Wigderson '01] and [Impagliazzo, Pudlák, and Sgall '99] are essentially best possible. More precisely, we establish that there are CNF formulas in constant width that have polynomial-size resolution refutations but require polynomial calculus degree scaling like the square root of the number of variables. Our presentation builds on material from [Stålmarck '96], [Bonet and Galesi '01], and [Galesi and Lauria '10], though we put the pieces together slightly differently (and use the polynomial calculus lower bounds proven in lectures 9 and 10).

We also review the paper [Atserias, Lauria, and Nordström '16], which proves that the naive counting argument that a CNF formula over n variables refutable in width w must have a resolution proof in size n^O(w) is tight. The same goes for the (much less naive) bound in polynomial calculus that if the PC refutation degree is d, then there is a PC refutation in size n^O(d) (and analogous results also hold for Sherali-Adams and sum-of-squares, but we do not go into any details about this in the lecture).

This is lecture 12 on the course "Proof complexity as a computational lens" (https://jakobnordstrom.se/teaching/pr...) given during the winter of 2025/26 at the University of Copenhagen and Lund University.


For more information about MIAO seminars and/or lectures, please visit https://jakobnordstrom.se/miao-seminars/ , or go to https://jakobnordstrom.se/miao-group/ to read more about the MIAO group.

#ProofComplexity