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

## No Access Until

##### Permanent Link(s)

## Collections

## Other Titles

## Author(s)

## 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 `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