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 i x 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 \(\frac{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)n− 1)64d(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].
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Buss, S., Grigoriev, D., Impagliazzo, R., Pitassi, T.: Linear gaps between degrees for the polynomial calculus modulo distinct primes. JCSS 62, 267–289 (2001)
Ben-Sasson, E., Wigderson, A.: Short proofs are narrow – resolution made simple. JACM 48(2) (2001)
Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. The Journal of Symbolic Logic 44(1), 36–50 (1979)
Dash, S.: Exponential lower bounds on the lengths of some classes of branch-and-cut proofs. IBM Research Report RC22575 (September 2002)
Grigoriev, D., Hirsch, E.A., Pasechnik, D.V.: Complexity of semialgebraic proofs. Moscow Mathematical Journal 2(4), 647–679 (2002)
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)
Haken, A.: The intractability of resolution. Theoretical Computer Science 39, 297–308 (1985)
Lovász, L., Schrijver, A.: Cones of matrices and set-functions and 0-1 optimization. SIAM J. Optimization 1(2), 166–190 (1991)
Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic 62(3), 981–998 (1997)
Razborov, A.A.: Lower bounds on the monotone complexity of some boolean functions. Doklady Akad. Nauk SSSR 282, 1033–1037 (1985)
Robinson, J.A.: The generalized resolution principle. Machine Intelligence 3, 77–94 (1968)
Tseitin, G.S.: On the complexity of derivation in the propositional calculus. Zapiski nauchnykh seminarov LOMI 8, 234–259 (1968); English translation of this volume: Consultants Bureau, N.Y., pp. 115–125 (1970)
Urquhart, A.: Hard examples for resolution. JACM 34(1), 209–219 (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hirsch, E.A., Nikolenko, S.I. (2005). Simulating Cutting Plane Proofs with Restricted Degree of Falsity by Resolution. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_10
Download citation
DOI: https://doi.org/10.1007/11499107_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)