Proof complexity as a computational lens lecture 20: Cutting planes, PB solving, and interpolation

Описание: Tuesday Jan 20, 2026
Proof complexity as a computational lens
Lecture 20: Cutting planes, proof systems for pseudo-Boolean solving, and more about feasible interpolation
(Jakob Nordström, University of Copenhagen and Lund University)

In this lecture, we define the cutting planes proof system, and review some basic facts about this proof system, such that it is exponentially stronger with respect to proof size/length than resolution. We then review some variants of cutting planes that are interesting to study in the context of pseudo-Boolean solving, namely with the saturation rule instead of division and with addition and multiplication steps restricted to so-called cancelling linear combination.

In the second half of the lecture, we refresh our memories about feasible interpolation, and then give an exposition of the result in [Pudlák '97] that the cutting planes proof system has monotone feasible interpolation. This yields exponential lower bounds for clique-colouring formulas (although we do not establish the lower bound for monotone real circuits that is required for a full proof of this result).

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