Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR05-006 | 28th December 2004 00:00

Simulating Cutting Plane proofs with restricted degree of falsity by Resolution


Authors: Edward Hirsch, Sergey I. Nikolenko
Publication: 17th January 2005 22:47
Downloads: 1403


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

Comment #1
Authors: Edward Hirsch, Sergey I. Nikolenko
Accepted on: 27th February 2005 20:03
Downloads: 1264


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.

ISSN 1433-8092 | Imprint