# A Satisfiability Tester for Non-Clausal Propositional Calculus

Conference paper

## Abstract

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.

## Preview

Unable to display preview. Download preview PDF.

## 9. References

- 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 - Coo71.Cook, S.A., “The complexity of theorem-proving procedures,” in
*Proc. Third Annual ACM Symposium on Theory of Computing*, (1971).Google Scholar - DaP60.Davis, M. and Putnam, H., “A computing procedure for quantification theory,”
*JACM*7(2?) pp. 201–215 (1960).MathSciNetCrossRefzbMATHGoogle Scholar - End72.Enderton, H.B.,
*A Mathematical Introduction to Logic*, Academic Press, New York, NY (1972).zbMATHGoogle Scholar - 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
- Ga177.Galil, Z., “On the complexity of regular resolution and the Davis-Putnam procedure,”
*Theoretical Computer Science*4 pp. 23–46 (1977).MathSciNetCrossRefzbMATHGoogle Scholar - Gol79.Goldberg, A.T., “On the complexity of the satisfiability problem,” NSO-16, Courant Institute of Mathematical Sciences, New York University (1979).Google Scholar
- Qui50.Quine, W.V.,
*Methods of logic.*Henry Holt (1950).Google Scholar - 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