Nowadays SAT solvers are able to solve problems with millions of variables, but some instances are still hard. While some formulas just require large time or memory to solve, other formulas allow to trade these resources. In the language of proof complexity, they have both short proofs and proofs in small space, but optimizing either measure blows up the other.
In this talk we will look at size-space trade-offs that hold not only for the resolution proof system, which captures most current solvers, 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).
