Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR03-041 | 29th May 2003 00:00

On Chvatal Rank and Cutting Planes Proofs



We study the Chv\'atal 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\'atal 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\'atal rank. The bound is
tight since we also prove a logarithmic upper bound.

ISSN 1433-8092 | Imprint