Simulating Cutting Plane proofs with restricted degree of falsity by resolution

Standard

Simulating Cutting Plane proofs with restricted degree of falsity by resolution. / Hirsch, Edward A.; Nikolenko, Sergey I.

In: Lecture Notes in Computer Science, Vol. 3569, 17.10.2005, p. 135-142.

Research output: Contribution to journal › Conference article › peer-review

BibTeX

@article{71e9b11baf054c57b70f7478b6f7ffad,

title = "Simulating Cutting Plane proofs with restricted degree of falsity by resolution",

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 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].",

author = "Hirsch, {Edward A.} and Nikolenko, {Sergey I.}",

year = "2005",

month = oct,

day = "17",

language = "English",

volume = "3569",

pages = "135--142",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer Nature",

note = "8th International Conference on Theory and Applications of Satisfiability Testing, SAT 2005 ; Conference date: 19-06-2005 Through 23-06-2005",

}

RIS

TY - JOUR

T1 - Simulating Cutting Plane proofs with restricted degree of falsity by resolution

AU - Hirsch, Edward A.

AU - Nikolenko, Sergey I.

PY - 2005/10/17

Y1 - 2005/10/17

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

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

UR - http://www.scopus.com/inward/record.url?scp=26444529458&partnerID=8YFLogxK

M3 - Conference article

AN - SCOPUS:26444529458

VL - 3569

SP - 135

EP - 142

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

T2 - 8th International Conference on Theory and Applications of Satisfiability Testing, SAT 2005

Y2 - 19 June 2005 through 23 June 2005

ER -

ID: 49828206