期刊名称:Electronic Colloquium on Computational Complexity
印刷版ISSN:1433-8092
出版年度:2003
卷号:2003
出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要: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.