Paper: Upper and lower bounds for tree-like cutting planes proofs (at LICS 1994)
Abstract
We study the complexity of cutting planes (CP) refutations, and tree-like CP refutations. Tree-like CP proofs are natural and still quite powerful. In particular, the propositional pigeonhole principle (PHP) has been shown to have polynomial-sized tree-like CP proofs. Our main result shows that a family of tautologies, introduced in this paper requires exponential-sized tree-like CP proofs. We obtain this result by introducing a new method which relates the size of a CP refutation to the communication complexity of a related search problem. Because these tautologies have polynomial-sized Frege proofs, it follows that tree-like CP cannot polynomially simulate Frege systems
BibTeX
@InProceedings{ImpagliazzoPitassiU-Upperandlowerbounds, author = {Russell Impagliazzo and Toniann Pitassi and Alasdair Urquhart}, title = {Upper and lower bounds for tree-like cutting planes proofs}, booktitle = {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)}, year = {1994}, month = {July}, pages = {220--228}, location = {Paris, France}, publisher = {IEEE Computer Society Press} }