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 ix 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].

Язык оригиналаанглийский
Страницы (с-по)135-142
Число страниц8
ЖурналLecture Notes in Computer Science
Том3569
СостояниеОпубликовано - 17 окт 2005
Событие8th International Conference on Theory and Applications of Satisfiability Testing, SAT 2005 - St Andrews, Великобритания
Продолжительность: 19 июн 200523 июн 2005

    Предметные области Scopus

  • Теоретические компьютерные науки
  • Компьютерные науки (все)

ID: 49828206