ECCC-Report TR05-006https://eccc.weizmann.ac.il/report/2005/006Comments and Revisions published for TR05-006en-usSun, 27 Feb 2005 20:03:28 +0200
Comment 1
| A stronger version of Corollary 1 Comment on: TR05-006 |
Edward Hirsch,
Sergey I. Nikolenko
https://eccc.weizmann.ac.il/report/2005/006#comment1We 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.
Sun, 27 Feb 2005 20:03:28 +0200https://eccc.weizmann.ac.il/report/2005/006#comment1
Paper TR05-006
| Simulating Cutting Plane proofs with restricted degree of falsity by Resolution |
Edward Hirsch,
Sergey I. Nikolenko
https://eccc.weizmann.ac.il/report/2005/006Goerdt (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.
Mon, 17 Jan 2005 22:47:27 +0200https://eccc.weizmann.ac.il/report/2005/006