Abstract:
Goerdt (1991) considered a weakened version of the Cutting Plane proof system with a restriction on the degree of falsity of intermediate inequalities. (The degree of falsity of an inequality written in the form $\sum a_ix_i+\sum b_i(1-x_i)\ge c,\ a_i,b_i\ge0$ is its constant term $c$.) He proved a superpolynomial lower bound on the proof length of Tseitin tautologies when the degree of falsity is bounded by $\frac{n}{\log^2n+1}$ ($n$ is the number of variables). In this short note we show that if the degree of falsity of a length $l$ proof is bounded by $b(n)=o(n)$, this proof can be easily transformed into a resolution proof of length $O(l\cdot{n\choose{b(n)-1}}64^{b(n)})$. Therefore, a superpolynomial bound on the proof length of Tseitin tautologies in this system for $b(n)=o(\frac{n}{\log n})$ follows immediately from Urquhart's (1987) lower bound for resolution proofs.

Comment #1 to TR05-006 | 27th February 2005 20:03

A stronger version of Corollary 1 Comment on: TR05-006

Abstract:
We show that the main theorem actually yields an exponential (rather than superpolynomial) lower bound for Cutting Plane proofs with degree of falsity bounded by a linear function of a number of variables.