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 ... more >>>

Having good algorithms to verify tautologies as efficiently as possible is of prime interest in different fields of computer science. In this paper we present an algorithm for finding Resolution refutations based on finding tree-like Res(k) refutations. The algorithm is based on the one of Beame and Pitassi \cite{BP96} for ... more >>>

We prove an exponential lower bound for tree-like Cutting Planes refutations of a set of clauses which has polynomial size resolution refutations. This implies an exponential separation between tree-like and dag-like proofs for both Cutting Planes and resolution; in both cases only superpolynomial separations were known before. In order to ... more >>>