zbMATH — the first resource for mathematics

On the complexity of cutting-plane proofs. (English) Zbl 0625.90056
As introduced by V. Chvatal [Discrete Math. 4, 305-337 (1973; Zbl 0253.05131)] cutting planes provide a canonical way of proving that every integral solution of a given system of linear inequalities satisfies another specified inequality. In this note we make several observations on the complexity of such proofs in general and when restricted to provide the unsatisfiability of formulae in the propositional calculus.

MSC:
 90C10 Integer programming 90C05 Linear programming 68Q25 Analysis of algorithms and problem complexity
Full Text:
References:
 [1] L. Babai, On Lovás” lattice reduction and the nearest lattice point, Combinatorica, to appear. · Zbl 0593.68030 [2] Bell, D.E., A theorem concerning the integer lattice, Stud. appl. math., 56, 187-188, (1977) · Zbl 0388.90051 [3] S.C. Boyd and W.R. Pulleyblank, Facet generating techniques, in preparation. · Zbl 1359.90113 [4] Chang, C.L.; Lee, R.C.T., Symbolic logic and mechanical theorem proving, (1973), Academic Press New York · Zbl 0241.68039 [5] Chvátal, V., Edmonds polytopes and a hierarchy of combinatorial problems, Discrete math., 4, 305-337, (1973) · Zbl 0253.05131 [6] Chvátal, V., Edmonds polytopes and weakly Hamiltonian graphs, Math. programming, 5, 29-40, (1973) · Zbl 0267.05118 [7] Chvátal, V., Cutting-plane proofs and the stability number of a graph, () · Zbl 0395.05047 [8] Chvátal, V., Cutting planes in combinatorics, () · Zbl 0581.05015 [9] Cook, S.A., Feasibly constructive proofs and the prop ositional calculus, (), 83-97 [10] Cook, S.A.; Reckhow, R.A., The relative efficiency of propositional proof systems, J. symbolic logic, 44, 36-50, (1977) · Zbl 0408.03044 [11] W. Cook, A.M.H. Gerards, A. Schrijver and É. Tardos, Sensitivity theorems in integer linear programming, Math. Programming, to appear. · Zbl 0648.90055 [12] Dowd, M., Propositional representation of arithmetic proofs, () · Zbl 1282.68112 [13] Gomory, R.E., An algorithm for integer solutions to linear programs, (), 269-302 [14] Goodstein, R.L., Recursive number theory, (1957), North-Holland Amsterdam · Zbl 0077.01401 [15] M. Grötschel, L. Lovász and A. Schrijver, The Ellipsoid Method and Combinatorial Optimization (Springer, Berlin, to appear). [16] Haken, A., The intractability of resolution, Theor. comput. sci., 39, 297-308, (1985) · Zbl 0586.03010 [17] J. Hastad, communicated by R. Kannan. [18] Helfrich, B., Eine beziehung zwischen konvexen mengen $$P ⊂ R\^{}\{2\}$$ und den gitterbasen von $$Z$$^{2}, (1985), Manuscript, Frankfurt, W. Germany [19] Hoffman, A.J., Binding constraints and Helly numbers, () · Zbl 0403.90056 [20] Kannan, R., Imkproved algorithms for integer programming and related lattice problems, (), 193-206 [21] R. Kannan and L. Lovász, to appear. [22] Lenstra, H.W., Integer programming with a fixed number of variables, Math. oper. res., 8, 538-548, (1983) · Zbl 0524.90067 [23] H.W. Lenstra, Jr. and C.P. Schnorr, On the successive minima of a pair of polar lattices, to appear. [24] Lovász, L., An algorithmic theory of numbers, graphs and convexity, () · Zbl 0606.68039 [25] Robinson, J.A., A machine-oriented logic based on the resolution principle, Jacm, 23-41, (1965) · Zbl 0139.12303 [26] H.E. Scarf, An observation on the structure of production sets with indivisibilities, Proc. Nat. Acad. Sci. (USA) 74, 3637-3641. · Zbl 0381.90081 [27] Schrijver, A., On cutting planes, Ann. discrete math., 9, 291-296, (1980) · Zbl 0441.90070 [28] Schrijver, A., Theory of linear and integer programming, (1986), Wiley Chichester · Zbl 0665.90063 [29] Todd, M.J., The number of necessary constraints in an integer program: a new proof of Scarf’s theorem, () [30] Tseitin, G.S., On the complexity of derivations in the propositional calculus, (), 115-125, translated from Russian
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.