Advertisement

Davis-Putnam resolution versus unrestricted resolution

  • Andreas Goerdt
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 440)

Abstract

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.

Keywords

Infinite Family Proof Tree Pigeonhole Principle Partial Truth Resolution Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Literature

  1. Aj 88.
    M. Ajtai, The complexity of the propositional pigeonhole principle, Proc. of the IEEE FOCS (1988).Google Scholar
  2. BuTu 88.
    S. R. Buss and G. Turán, Resolution proofs of generalized pigeonhole principles, Theoret. Comp. Sci. 62 (1988) 311–317.Google Scholar
  3. ChSz 88.
    V. Chvátal and E. Szemeredi, Many hard examples for resolution, J. Assoc. Comput. Mach. 35 (4) (1988) 759–768.Google Scholar
  4. 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
  5. DaPu 60.
    M. Davis and H. Putnam, A computing procedure for quantification theory, JACM 7 (1960) 201–215.CrossRefGoogle Scholar
  6. Gal 77.
    Z. Galil, On the complexity of regular resolution and the Davis-Putnam procedure, Theoret. Comput. Sci. 4 (1977) 23–46.Google Scholar
  7. Go 89.
    A. Goerdt, Unrestricted resolution versus N-resolution, Technical report, Universität-GH-Duisburg (1989) submitted.Google Scholar
  8. Ha 85.
    A. Haken, The intractability of resolution, Theoret. Comput. Sci 39 (1985) 297–308.CrossRefGoogle Scholar
  9. Re 75.
    R. A. Reckhow, On the lengths of proofs in the propositional calculus, Ph. D. thesis, University of Toronto (1975).Google Scholar
  10. Ur 87.
    A. Urquhart, Hard examples for resolution, J. Assoc. Comput. Mach. 34 (1987) 209–219.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Andreas Goerdt
    • 1
  1. 1.Universität -GH- Duisburg Fachbereich Mathematik Fachgebiet Praktische InformatikDuisburgWest-Germany

Personalised recommendations