A weakened version of the Cutting Plane (CP) proof system with a restriction on the degree of falsity of intermediate inequalities was introduced by Goerdt. He proved an exponential lower bound for CP proofs with degree of falsity bounded by n/log2n+1 where n is the number of variables. Hirsch and Nikolenko strengthened this result by establishing a direct connection between CP and Resolution proofs. This result implies an exponential lower bound on the proof length of the Tseitin-Urquhart tautologies, when the degree of falsity is bounded by cn for some constant c. In this paper we generalize this result for extensions of Lovasz-Schrijver calculi (LS), namely for LSk+CPk proof systems introduced by Grigoriev et al. We show that any LSk+CPk proof with bounded degree of falsity can be transformed into a Res(k) proof. We also prove lower and upper bounds for the new system.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings
PublisherSpringer Nature
Pages11-21
Number of pages11
ISBN (Print)3540372067, 9783540372066
StatePublished - 1 Jan 2006
Event9th International Conference on Theory and Applications of Satisfiability Testing, SAT 2006 - Seattle, WA, United States
Duration: 12 Aug 200615 Aug 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4121 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Conference on Theory and Applications of Satisfiability Testing, SAT 2006
Country/TerritoryUnited States
CitySeattle, WA
Period12/08/0615/08/06

    Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

ID: 49824989