You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Complexity of Semialgebraic Proofs with Restricted Degree of Falsity12

Article type: Research Article

Authors: Hirsch, Edward A. | Kojevnikov, Arist | Kulikov, Alexander S. | Nikolenko, Sergey I.

Affiliations: Steklov Institute of Mathematics at St. Petersburg, 27 Fontanka, 191023 St. Petersburg, Russia. E-mails: arist@logic.pdmi.ras.ru, kulikov@logic.pdmi.ras.ru, sergey@logic.pdmi.ras.ru

Note: [1] Supported in part by the Russian Foundation for Basic Research (grants 05-01-00932, 06-01-00502, 06-01-00584), RAS Program for Fundamental Research (“Modern Problems of Theoretical Mathematics”), Russian presidential leading science school support grant N.Sh. 4392.2008.1, and Russian Science Support Foundation. The first author is also supported by the Dynasty Foundation Fellowship.

Note: [2] This is a joint journal version of two papers earlier presented at SAT 2005 and SAT 2006 [9, 11].

Keywords: propositional proof system, lower bound, algebraic proof system, Cutting Planes, Lovasz-Schrijver proof system

DOI: 10.3233/SAT190062

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 6, no. 1-3, pp. 53-69, 2010

Received 1 January 2008
|
Revision received 1 July 2008
|
Published: 1 November 2008
Get PDF open access

Abstract

The degree of falsity of an inequality in Boolean variables shows how many variables are enough to substitute in order to satisfy the inequality. Goerdt introduced a weakened version of the Cutting Plane (CP) proof system with a restriction on the degree of falsity of intermediate inequalities [6]. He proved an exponential lower bound for CP proofs with degree of falsity bounded by nlog2n+1, where n is the number of variables.

In this paper we strengthen this result by establishing a direct connection between CP and Resolution proofs. This result implies an exponential lower bound on the proof length of Tseitin-Urquhart tautologies when the degree of falsity is bounded by cn for some constant c. We also generalize the notion of degree of falsity for extensions of Lovász-Schrijver calculi (LS), namely for LSk+CPk proof systems introduced by Grigoriev et al. [8]. 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 on the proof length of tautologies in LSk+CPk with bounded degree of falsity.

Show more