Published: March 25, 2006
Abstract: [Plain Text Version]
We present a new method for proving rank lower bounds for the cutting planes procedures of Gomory and Chvátal ($\GC$) and Lovász and Schrijver ($\LS$), when viewed as proof systems for unsatisfiability. We apply this method to obtain the following new results: First, we prove near-optimal rank bounds for $\GC$ and $\LS$ proofs for several prominent unsatisfiable CNF examples, including random kCNF formulas and the Tseitin graph formulas. It follows from these lower bounds that a linear number of rounds of $\GC$ or $\LS$ procedures when applied to the standard MAXSAT linear relaxation does not reduce the integrality gap. Second, we give unsatisfiable examples that have constant rank $\GC$ and $\LS$ proofs but that require linear rank Resolution proofs. Third, we give examples where the $\GC$ rank is $O(\log n)$ but the $\LS$ rank is linear. Finally, we address the question of size versus rank; we show that, for both proof systems, rank does not accurately reflect proof size. Specifically, there are examples which have polynomial-size $\GC$/$\LS$ proofs but require linear rank.