The expected complexity of analytic tableaux analyses in propositional calculus.
J. M. Plotkin, John W. Rosenthal · Notre Dame Journal of Formal Logic · 1982
We subscribe to the philosophy that comparison of the expected complexity of algorithms may often provide a better indication of relative efficiency than a comparison of the worst case complexity (cf., e.g., Knuth [10]).Research into algorithms that are efficient on the average has burgeoned in recent years.Karp in [9] discusses such algorithms for several graph theoretic problems.For example Posa [13], Angluin and Valiant [1], and Karp [9] show there are polynomial time algorithms that almost surely find Hamiltonian circuits if they exist.In the survey [9] Karp remarks that no fast-average-time algorithms are known for such problems as constructing minimum colorings or maximum cliques.We close by mentioning a negative result of Chvatal.In [4] he shows that Tarjan-Trojanowski type algorithms for finding the stability of a graph run in average exponential time.The purpose of our article is to illustrate techniques useful in determining the expected complexity of (a variant of) the analytic tableau algorithm for the satisfiability problem of propositional calculus.Before we proceed it is important to mention the work of Goldberg [5] on the Davis-Putnam procedure for testing propositional satisfiability.In particular he showed that when the uniform distribution is placed on the set of problem instances, the expected time of the Davis-Putnam procedure is O(kr 2 ) where r is the number of clauses in the given set and k is the number of distinct atoms.*We wish to thank our colleague E. M. Palmer for many helpful suggestions, especially of useful references in combinatorics.