TR05-006 Authors: Edward Hirsch, Sergey I. Nikolenko

Publication: 17th January 2005 22:47

Downloads: 1685

Keywords:

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 Authors: Edward Hirsch, Sergey I. Nikolenko

Accepted on: 27th February 2005 20:03

Downloads: 1563

Keywords:

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.