Davis-Putnam resolution versus unrestricted resolution
A resolution proof of an unsatisfiable propositional formula in conjunctive normalform 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. In the terminology of CoRe 79, definition 1.5: Davis-Putnam resolution does not p-simulate unrestricted resolution.
KeywordsInfinite Family Proof Tree Pigeonhole Principle Partial Truth Resolution Rule
Unable to display preview. Download preview PDF.
- Aj 88.M. Ajtai, The complexity of the propositional pigeonhole principle, Proc. of the IEEE FOCS (1988).Google Scholar
- BuTu 88.S. R. Buss and G. Turán, Resolution proofs of generalized pigeonhole principles, Theoret. Comp. Sci. 62 (1988) 311–317.Google Scholar
- ChSz 88.V. Chvátal and E. Szemeredi, Many hard examples for resolution, J. Assoc. Comput. Mach. 35 (4) (1988) 759–768.Google Scholar
- CoRe 79.S. A. Cook and R. A. Reckhow, The relative efficiency of propositional proof systems, J. Symbolic Logic 44(1) (1979) 36–50.Google Scholar
- DaPu 60.
- Gal 77.Z. Galil, On the complexity of regular resolution and the Davis-Putnam procedure, Theoret. Comput. Sci. 4 (1977) 23–46.Google Scholar
- Go 89.A. Goerdt, Unrestricted resolution versus N-resolution, Technical report, Universität-GH-Duisburg (1989) submitted.Google Scholar
- Ha 85.
- Re 75.R. A. Reckhow, On the lengths of proofs in the propositional calculus, Ph. D. thesis, University of Toronto (1975).Google Scholar
- Ur 87.A. Urquhart, Hard examples for resolution, J. Assoc. Comput. Mach. 34 (1987) 209–219.Google Scholar