TY - JOUR
T1 - Lower bounds for cutting planes proofs with small coefficients
AU - Bonet, Maria
AU - Pitassi, Toniann
AU - Raz, Ran
N1 - Copyright:
Copyright 2017 Elsevier B.V., All rights reserved.
PY - 1997/9
Y1 - 1997/9
N2 - We consider small-weight Cutting Planes (CP*) proofs: that is, Cutting Planes (CP) proofs with coefficients up to 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.
AB - We consider small-weight Cutting Planes (CP*) proofs: that is, Cutting Planes (CP) proofs with coefficients up to 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.
UR - http://www.scopus.com/inward/record.url?scp=0031481402&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0031481402&partnerID=8YFLogxK
U2 - 10.2307/2275569
DO - 10.2307/2275569
M3 - Article
AN - SCOPUS:0031481402
SN - 0022-4812
VL - 62
SP - 708
EP - 728
JO - Journal of Symbolic Logic
JF - Journal of Symbolic Logic
IS - 3
ER -