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

Abstract

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 $i^{th}$ element of the vector is equal to +, -, 0, or 1, according as the $i^{th}$ 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^{+} greater than S^{+}$ and $R^{-} less than S^{-}$, or $R^{+} less than S^{+}$ and $R^{-} greater than S^{-}$. The former pair is denoted $``r \ogeq s''; \ogeq$ is a strict ordering of clause-types, which is total for RSDNF's. If $r \ogeq s$ and for no $p$ of $E$ is $r \ogeq p \ogeq s$, 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^{+} + t^{-} \leq V-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.