Proof complexity as a computational lens lecture 13: Space complexity; resolution space vs. width

Описание: Tuesday Dec 9, 2025
Proof complexity as a computational lens
Lecture 13: Space complexity; resolution clause space vs. width
(Jakob Nordström, University of Copenhagen and Lund University)

In this lecture, we commence our study of space, i.e., the memory consumption of proofs, in proof complexity. We define the measures of clause space, variable space, and total space for resolution. We also introduce black and black-white pebbling and discuss some of the ways in which pebbling is related to proof space complexity, in particular, via so-called pebbling formulas or pebbling contradictions.

We review some foundational results, such as that the refutation clause space of any unsatisfiable CNF formula is at most linear in the number of clauses and variables, and that if a formula has a resolution refutation in length L, then it can also be refuted in clause space O(L / log L). We then present the theorem in [Atserias and Dalmau '08] that clause space provides an upper bound on width for resolution refutations. Finally, we show that there are strong trade-offs between clause space and width in that there are formulas that are refutable in resolution both in constant clause space and in constant width, but where optimizing one of these measures in any refutation leads to essentially worst-case behaviour for the other measure, as shown in [Ben-Sasson '09]. Throughout the lecture, we try to highlight a number of open problems, some of them regarding even fairly basic aspects of resolution and pebbling space complexity.

This is lecture 13 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