Abstract
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 \({\frac{n}{\log^{2n}+1}}\), where n is the number of variables. Hirsch and Nikolenko strengthened this result by establishing a direct connection between CP and Res(k) 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 Lovász-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.
Supported in part by INTAS (grants 04-77-7173, 04-83-3836, 05-109-5352), RFBR (grants 05-01-00932, 06-01-00502, 06-01-00584), RAS Program for Fundamental Research (“Modern Problems of Theoretical Mathematics”), and Russian Science Support Foundation.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Cook, S.A., Reckhow, R.A.: The Relative Efficiency of Propositional Proof Systems. The Journal of Symbolic Logic 44(1), 36–50 (1979)
Goerdt, A.: The Cutting Plane Proof System with Bounded Degree of Falsity. In: Kleine Büning, H., Jäger, G., Börger, E., Richter, M.M. (eds.) CSL 1991. LNCS, vol. 626, pp. 119–133. Springer, Heidelberg (1992)
Robinson, J.A.: The generalized resolution principle. Machine Intelligence 3, 77–94 (1968)
KrajĂÄŤek, J.: On the weak pigeonhole principle. Fundamenta Mathematicæ 170(1-3), 123–140 (2001)
Gomory, R.E.: An algorithm for integer solutions of linear programs. In: Graves, R.L., Wolfe, P. (eds.) Recent Advances in Mathematical Programming, pp. 269–302. McGraw-Hill, New York (1963)
Cook, W., Coullard, C.R., Turán, G.: On the complexity of cutting-plane proofs. Discrete Applied Mathematics 18(1), 25–38 (1987)
Grigoriev, D., Hirsch, E.A., Pasechnik, D.V.: Complexity of semialgebraic proofs. Moscow Mathematical Journal 2(4), 647–679 (2002)
Atserias, A., Bonet, M.L.: On the automatizability of resolution and related propositional proof systems. Information and Computation 189(2), 182–201 (2004)
Hirsch, E.A., Nikolenko, S.I.: Simulating Cutting Plane proofs with restricted degree of falsity by Resolution. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 135–142. Springer, Heidelberg (2005)
Segerlind, N., Buss, S.R., Impagliazzo, R.: A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution. SIAM Journal on Computing 33(5), 1171–1200 (2004)
Alekhnovich, M., Ben-Sasson, E., Razborov, A.A., Wigderson, A.: Pseudorandom generators in propositional proof complexity. SIAM Journal on Computing 34(1), 67–88 (2004)
Alekhnovich, M.: Lower bounds for k-DNF resolution on random 3-CNFs. In: STOC 2005: Proceedings of the thirty-seventh annual ACM symposium on Theory of computing, pp. 251–256. ACM Press, New York (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kojevnikov, A., Kulikov, A.S. (2006). Complexity of Semialgebraic Proofs with Restricted Degree of Falsity. In: Biere, A., Gomes, C.P. (eds) Theory and Applications of Satisfiability Testing - SAT 2006. SAT 2006. Lecture Notes in Computer Science, vol 4121. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814948_3
Download citation
DOI: https://doi.org/10.1007/11814948_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37206-6
Online ISBN: 978-3-540-37207-3
eBook Packages: Computer ScienceComputer Science (R0)