On the rank of cutting-plane proof systems

We introduce a natural abstraction of propositional proof systems that are based on cutting planes. This new class of proof systems includes well-known operators such as Gomory-Chvátal cuts, lift-and-project cuts, Sherali-Adams cuts (for a fixed hierarchy level d), and split cuts. The rank of such a proof system corresponds to the number of rounds needed to show the nonexistence of integral solutions. We exhibit a family of polytopes without integral points contained in the n-dimensional 0/1-cube that has rank Ω(n/log n) for any proof system in our class. In fact, we show that whenever a specific cutting-plane based proof system has (maximal) rank n on a particular family of instances, then any cutting-plane proof system in our class has rank Ω(n/log n) for this family. This shows that the rank complexity of worst-case instances is intrinsic to the problem, and does not depend on specific cutting-plane proof systems, except for log factors. We also construct a new cutting-plane proof system that has worst-case rank O(n/log n) for any polytope without integral points, implying that the universal lower bound is essentially tight.