zbMATH — the first resource for mathematics

A satisfiability tester for non-clausal propositional calculus. (English) Zbl 0658.68107
An algorithm for satisfiability testing in propositional calculus with worst case complexity \(2^{(0.25+\epsilon)L}\) is presented, where L can be either the length of the input or the number of occurrences of literals in the expression. The algorithm proceeds by a careful choice of the “branch” variable and has the important feature that it does not need the testing expression to be in any normal form.
Reviewer: M.Zimand

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
PDF BibTeX Cite
Full Text: DOI
[1] Aho, A.V.; Hopcroft, J.E.; Ullman, J.D., ()
[2] Cook, S.A., The complexity of theorem-proving procedures, () · Zbl 0363.68125
[3] Davis, M.; Putnam, H., A computing procedure for quantification theory, J. assoc. comput. Mach., 7, 201-215, (1960) · Zbl 0212.34203
[4] Enderton, H.B., ()
[5] Galil, Z., (), TR 75-239
[6] Galil, Z., On the complexity of regular resolution and the Davis-Putnam procedure, Theoret. comput. sci., 4, 23-46, (1977) · Zbl 0385.68048
[7] Goldberg, A.T., (), NSO-16
[8] Quine, W.V., ()
[9] Tseitin, G.S., On the complexity of derivations in the propositional calculus, (), 115-125, Part II
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.