LOWER BOUNDS FOR CUTTING PLANES PROOFS WITH SMALL COEFFICIENTS

We consider small-weight Cutting Planes (CP) proofs; that is, Cutting Planes (CP) proofs with coefficients up to Poly(n). We use the well k nown lower bounds for monotone complexity to prove an exponential lowe r bound for the length of CP proofs, for ii family of tautologies bas ed on the clique function. Because Resolution is a special case of sma ll-weight CP, our method also gives a new and simpler exponential lowe r bound for Resolution. We also prove the following two theorems: (I) Tree-like CP proofs cannot polynomially simulate non-tree-like CP* pr oofs. (2) Tree-like CP proofs and Bounded-depth-Frege proofs cannot p olynomially simulate each other Our proofs also work for some generali zations of the CP pl oof system. In particular, they work for CP* wit h a deduction rule, and also for any proof system that allows any form ula with small communication complexity, and any set of sound rules of inference.