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