Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR05-006 | 28th December 2004 00:00

Simulating Cutting Plane proofs with restricted degree of falsity by Resolution

RSS-Feed




TR05-006
Authors: Edward Hirsch, Sergey I. Nikolenko
Publication: 17th January 2005 22:47
Downloads: 2200
Keywords: 


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(s):

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: 2432
Keywords: 


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.




ISSN 1433-8092 | Imprint