A Satisfiability Tester for Non-Clausal Propositional Calculus
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.
- Coo71.Cook, S.A., “The complexity of theorem-proving procedures,” in Proc. Third Annual ACM Symposium on Theory of Computing, (1971).Google 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
- 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