Logic in Computer Science (LICS 1994)

Paper: Upper and lower bounds for tree-like cutting planes proofs (at LICS 1994)

Authors: Russell Impagliazzo Toniann Pitassi Alasdair Urquhart

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 Symp. on Logic in Computer Science, {LICS} 1994},
    year =	 1994,
    editor =	 {Samson Abramsky},
    month =	 {July}, 
    pages =      {220--228},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }