Abstract

We consider small-weight Cutting Planes (CP * ) proofs; that is, Cutting Planes (CP) proofs with coefficients up to $\operatorname{Poly}(n)$ . We use the well known lower bounds for monotone complexity to prove an exponential lower bound for the length of CP * proofs, for a family of tautologies based on the clique function. Because Resolution is a special case of small-weight CP, our method also gives a new and simpler exponential lower bound for Resolution. We also prove the following two theorems: (1) Tree-like CP * proofs cannot polynomially simulate non-tree-like CP * proofs. (2) Tree-like (CP * proofs and Bounded-depth-Frege proofs cannot polynomially simulate each other. Our proofs also work for some generalizations of the CP * proof system. In particular, they work for CP * with a deduction rule, and also for any proof system that allows any formula with small communication complexity, and any set of sound rules of inference