We obtain the first true size-space trade-offs for the cutting planes proof system, where the upper bounds hold for size and total space for derivations with constant-size coefficients, and the lower bounds apply to length and formula space (i.e., number of inequalities in memory) even for derivations with exponentially large coefficients. These are also the first trade-offs to hold uniformly for resolution, polynomial calculus and cutting planes, thus capturing the main methods of reasoning used in current state-of-the-art SAT solvers.

We prove our results by a reduction to communication lower bounds in a round-efficient version of the real communication model of [Krají$\check{c}$ek '98], drawing on and extending techniques in [Raz and McKenzie '99] and [Göös et al. '15]. Such lower bounds are in turn established by a reduction to trade-offs between cost and number of rounds in the game of [Dymond and Tompa '85] played on directed acyclic graphs.

As a by-product of the techniques developed to show these proof complexity trade-off results, we also obtain a separation between $\textrm{monotone-AC}^{i-1}$ and $\textrm{monotone-NC}^{i}$, and an exponential separation between $\textrm{monotone-AC}^{i-1}$ and $\textrm{monotone-AC}^{i}$, improving exponentially over the superpolynomial separation in [Raz and McKenzie '99].