Lower Bounds for Cutting Planes Proofs with Small Coefficients
Bonet, Maria ; Pitassi, Toniann ; Raz, Ran
J. Symbolic Logic, Tome 62 (1997) no. 1, p. 708-728 / Harvested from Project Euclid
We consider small-weight Cutting Planes $(\mathrm{CP}^\ast)$ 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 $\mathrm{CP}^\ast$ 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 $\mathrm{CP}^\ast$ proofs cannot polynomially simulate non-tree-like $\mathrm{CP}^\ast$ proofs. (2) Tree-like $(\mathrm{CP}^\ast$ proofs and Bounded-depth-Frege proofs cannot polynomially simulate each other. Our proofs also work for some generalizations of the $\mathrm{CP}^\ast$ proof system. In particular, they work for $\mathrm{CP}^\ast$ 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.
Publié le : 1997-09-14
Classification: 
@article{1183745294,
     author = {Bonet, Maria and Pitassi, Toniann and Raz, Ran},
     title = {Lower Bounds for Cutting Planes Proofs with Small Coefficients},
     journal = {J. Symbolic Logic},
     volume = {62},
     number = {1},
     year = {1997},
     pages = { 708-728},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183745294}
}
Bonet, Maria; Pitassi, Toniann; Raz, Ran. Lower Bounds for Cutting Planes Proofs with Small Coefficients. J. Symbolic Logic, Tome 62 (1997) no. 1, pp.  708-728. http://gdmltest.u-ga.fr/item/1183745294/