A Rank Lower Bound for Cutting Planes Proofs of Ramsey’s Theorem

Abstract

Ramsey’s Theorem is a cornerstone of combinatorics and logic. In its simplest formulation it says that for every k > 0 and s > 0, there is a minimum number r ( k , s ) such that any simple graph with at least r ( k , s ) vertices contains either a clique of size k or an independent set of size s . We study the complexity of proving upper bounds for the number r ( k , k ). In particular, we focus on the propositional proof system cutting planes; we show that any cutting plane proof of the upper bound “ r ( k , k ) ⩽ 4 k ” requires high rank. In order to do that we show a protection lemma which could be of independent interest.