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átal 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 opposite 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..