### Abstract

Goerdt [Goe91] 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 ∑ a _{i}x _{i} + ∑ b _{i}(1 - x _{i}) ≥ A, a _{i}, b _{i} ≥ 0 is its constant term A.) He proved a superpolynomial lower bound on the proof length of Tseitin-Urquhart tautologies when the degree of falsity is bounded by n/log ^{2} n+1 (n is the number of variables). In this paper we show that if the degree of falsity of a Cutting Planes proof Π is bounded by d(n) ≤ n/2, this proof can be easily transformed into a resolution proof of length at most |Π|·( _{d(n)-1} ^{n})64 ^{d(n)}. Therefore, an exponential bound on the proof length of Tseitin-Urquhart tautologies in this system for d(n) ≤ cn for an appropriate constant c > 0 follows immediately from Urquhart's lower bound for resolution proofs [Urq87].

Original language | English |
---|---|

Pages (from-to) | 135-142 |

Number of pages | 8 |

Journal | Lecture Notes in Computer Science |

Volume | 3569 |

Publication status | Published - 17 Oct 2005 |

Event | 8th International Conference on Theory and Applications of Satisfiability Testing, SAT 2005 - St Andrews Duration: 19 Jun 2005 → 23 Jun 2005 |

### Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)