×

Davis-Putnam resolution versus unrestricted resolution. (English) Zbl 0865.03010

Summary: A resolution proof of an unsatisfiable propositional formula in conjunctive normal form is a “Davis-Putnam resolution proof” iff there exists a sequence of the variables of the formula such that \(x\) is eliminated (with the resolution rule) before \(y\) on any branch of the proof tree representing the resolution proof, only if \(x\) is before \(y\) in this sequence. Davis-Putnam resolution is one of several resolution restrictions. It is complete.
We present an infinite family of unsatisfiable propositional formulas and show: These formulas have unrestricted resolution proofs whose length is polynomial in their size. All Davis-Putnam resolution proofs of these formulas are of superpolynomial length.

MSC:

03B35 Mechanization of proofs and logical operations
03B05 Classical propositional logic
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] M. Ajtai, The complexity of the propositional pigeonhole principle,Proc. 29th IEEE Symp. on Foundations of Computer Science (1988) p. 346-355.
[2] S.R. Buss and G. Tur?n, Resolution proofs of generalized pigeonhole principles, Theor. Comput. Sci. 62 (1988) 311-317. · Zbl 0709.03006
[3] V. Chv?tal and E. Szemeredi, Many hard examples for resolution, J. ACM 35 (1988) 759-768. · Zbl 0712.03008
[4] S.A. Cook and R.A. Reckhow, The relative efficiency of propositional proof systems, J. Symbolic Logic 44(1) (1979) 36-50. · Zbl 0408.03044
[5] M. Davis and H. Putnam, A computing procedure for quantification theory, J. ACM 7 (1960) 201-215. · Zbl 0212.34203
[6] Z. Galil, On the complexity of regular resolution and the Davis-Putnam procedure, Theor. Comput. Sci. 4 (1977) 23-46. · Zbl 0385.68048
[7] A. Goerdt, Unrestricted resolution versusN-resolution, Theor. Comput. Sci., to appear. · Zbl 0745.68093
[8] A. Haken, The intractability of resolution, Theor. Comput. Sci. 39 (1985) 297-308. · Zbl 0586.03010
[9] R.A. Reckhow, On the lengths of proofs in the propositional calculus, Ph. D. thesis, University of Toronto (1975). · Zbl 0375.02004
[10] A. Urquhart, Hard examples for resolution, J. ACM 34 (1987) 209-219. · Zbl 0639.68093
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.