On Chvátal Rank and Cutting Planes Proofs
Albert Atserias, Marı́a Luisa Bonet, Jordi Levy · 2003
We study the Chvatal rank of polytopes as a complexity measure of unsatisfiable sets of clauses. We discuss the relationship between the Chvatal rank and the minimum refutation length and height in the cutting planes proof system. The main technical result is a general technique for deriving Chvatal 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 Chvatal rank. The bound is tight since we also prove a logarithmic upper bound. We also apply the technique to the polytope of the Ramsey Principle and obtain a loglogarithmic rank lower bound.