A Satisfiability Tester for Non-Clausal Propositional Calculus

  • Allen Van Gelder
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


An algorithm for satisfiability testing in the propositional calculus with a worst case running time that grows at a rate less than 2(.25+ε)L is described, where L can be either the length of the input expression or the number of occurrences of literals (i.e., leaves) in it. This represents a new upper bound on the complexity of non-clausal satisfiability testing. The performance is achieved by using lemmas concerning assignments and pruning that preserve satisfiability, together with choosing a “good” variable upon which to recur. For expressions in clause form, it is shown that the Davis-Putnam procedure satisfies the same upper bound.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

9. References

  1. AHU74.
    Aho, A.V., Hopcroft, J.E., and Ullman, J.D., The design and analysis of computer algorithms, Addison-Wesley, Reading, MA (1974).zbMATHGoogle Scholar
  2. Coo71.
    Cook, S.A., “The complexity of theorem-proving procedures,” in Proc. Third Annual ACM Symposium on Theory of Computing, (1971).Google Scholar
  3. DaP60.
    Davis, M. and Putnam, H., “A computing procedure for quantification theory,” JACM 7(2?) pp. 201–215 (1960).MathSciNetCrossRefzbMATHGoogle Scholar
  4. End72.
    Enderton, H.B., A Mathematical Introduction to Logic, Academic Press, New York, NY (1972).zbMATHGoogle Scholar
  5. Gal75.
    Galil, Z., “The complexity of resolution procedures for theorem proving in the propositonal calculus,” TR 75-239, Department of Computer Science, Cornell University (1975).Google Scholar
  6. Ga177.
    Galil, Z., “On the complexity of regular resolution and the Davis-Putnam procedure,” Theoretical Computer Science 4 pp. 23–46 (1977).MathSciNetCrossRefzbMATHGoogle Scholar
  7. Gol79.
    Goldberg, A.T., “On the complexity of the satisfiability problem,” NSO-16, Courant Institute of Mathematical Sciences, New York University (1979).Google Scholar
  8. Qui50.
    Quine, W.V., Methods of logic. Henry Holt (1950).Google Scholar
  9. Tse68.
    Tseitin, G.S., “On the complexity of derivations in the propositional calculus,” pp. 115–125 in Studies in Constructive Mathematics and Mathematical Logic, Part II, ed. Slisenko, A.O., (1968).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Allen Van Gelder
    • 1
  1. 1.Computer Science DepartmentStanford UniversityStanfordUSA

Personalised recommendations