Abstract. In 1980 Monien and Speckenmeyer proved that satisfiability of a propositional formula consisting of K clauses (of arbitrary length) can be checked in time of the order 2^K/3. Recently Kullmann and Luckhardt proved the worst-case upper bound 2^L/9, where L is the length of the input formula. The algorithms leading to these bounds are based on the splitting method which goes back to the Davis-Putnam procedure. Transformation rules (pure literal elimination, unit propagation etc.) constitute a substantial part of this method. In this paper we present a new transformation rule and two algorithms using this rule. We prove that these algorithms have the worst-case upper bounds 2^0.30897K and 2^0.10299L respectively.

Full text (draft): [ .ps.gz (115 Kb) ]