On Chvátal Rank and Cutting Planes Proofs

We study the Chvátal rank of polytopes as a complexity measure of unsatisfiable sets of clauses. Our first result establishes a connection between the Chv'atal rank and the minimum refutation length in the cutting planes proof system. The result implies that length lower bounds for cutting planes, or even for tree-like cutting planes, imply rank lower bounds. We also show that the converse implication is false. Rank lower bounds don't imply size lower bounds. In fact we give an example of a class of formulas that have hight rank and small size. A corollary of the previous results is that cutting planes proofs cannot be balanced. We also introduce a general technique for deriving Chvátal rank lower bounds directly from the syntactical form of the inequalities. We apply this technique to show that the polytope of the Pigeonhole Principle requires logarithmic Chvátal rank. The bound is tight since we also prove a logarithmic upper bound.