Memory usage is a limit of SAT solvers that proof complexity models in terms of the space measure. While some formulas just require large time or memory to solve, other formulas allow to trade these resources. This is, they have both short proofs and proofs in small space, but optimizing either measure blows up the other.

In this talk we will show size-space trade-offs that hold not only for the resolution proof system, which captures CDCL, but for polynomial calculus and cutting planes, which capture algebraic and pseudo-boolean reasoning respectively. The proof goes through communication complexity, and a key insight is to use a model of communication that captures short cutting planes proofs: communication with limited rounds and with real numbers.

Joint work with Susanna F. de Rezende and Jakob Nordström.