A Polynomial Bound on the Complexity of the Davis-PutnamAlgorithm Applied to Symmetrizable Propositions

Other Titles


The problem considered is the relation of minimal computation space to minimal computation time; more specifically, it is desired to determine the time complexity of the tautology problem for propositional logic; the space complexity is known to be linear. This is of special interest in view of Stephen Cook's p-reducibility theorem (May, 1971 ACM Symposium). Algorithms considered are the analytic tableau method, which appears to be inalterably exponential in space and time, and the Davis-Putnam algorithm, part of a resolution procedure introduced in JACM in 1960. Although the algorithm as stated has been shown to be exponential, the known examples are disposed of by (1) locally optimizing the choice of elimination variable and (2) using the subsumption rule (absorption rule), which asserts that if any clause is identical to a subclause of another clause, the larger clause may be deleted. An algebraic notation is developed which makes it clear that Davis and Putnam's Rules 1 and 2 are special cases of Rule 3 plus local optimization and subsumption. The algebraic notation consists of using vectors to represent clauses; the ith element of the vector is equal to +, -, 0, or 1, according as the ith variable occurs positively, negatively, or not at all. This notation is used in an APL computer program; by using 01,10,00, and 11 to represent +, -, 0, and 1, the program can be written entirely in terms of APL logical operators on arrays, with loops needed only because of size limitations, at a considerable savings in time and space compared to a list representation of the formula, for up to about twenty variables. The proof in brief of the polynomial special-case bound: Call a DNF formula reduced'' if the subsumption rule will delete no clauses; call it symmetric'' if it is invariant (as a set of clauses) under interchange of variable names. For any clause R, let R+ be the number of positive literals in R and R the number of negated literals. Call (R+,R) the (clause-)type of R. A symmetric formula A then satisfies the property that if (R+,R) is the type of some clause in A, then every clause of type (R+,R) is also a clause of A. An algebra of clause-types is developed; it is easily shown that if r=(R+,R) and s=(S+,S) are unequal types of a reduced symmetric DNF formula (RSDNF), then either R+greaterthanS+ and RlessthanS, or R+lessthanS+ and RgreaterthanS. The former pair is denoted ‘‘r\ogeqs″;\ogeq is a strict ordering of clause-types, which is total for RSDNF's. If r\ogeqs and for no p of E is r\ogeqp\ogeqs, say r adj s (in E). Denote by PROD(A) the result of one iteration of the Davis-Putnam algorithm with subsumption. Let E be and RSDNF in V variables. The t is a type of PROD(E) if either (1) t is a type of E (with t++tV−1), and for no x or y is (t++1,x) or (y,t+1) a type of E; or (2) t=(r+−1,s−1), with r adj s in E. It is further shown that if r adj s in PROD(E), then either r+=s++1, or s=r+1, or (r+−1,s−1) is not a type of PROD(PROD(E)). A simple combinatorial argument then shows that each type of PROD(PROD(E)) has fewer clauses than some type of PROD(E). The polynomial bound is then immediate, since there are at most V+1 types in any RSDNF formula in V variables, and the number of varialbles decreases with each iteration, and there can be at most V iterations. The extension to symmetrizable is trivial.

Journal / Series

Volume & Issue



Date Issued



Cornell University


computer science; technical report


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Committee Co-Chair

Committee Member

Degree Discipline

Degree Name

Degree Level

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)


Link(s) to Reference(s)

Previously Published As

Government Document




Other Identifiers


Rights URI


technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record