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 2K / 3. Recently Kullmann and Luckhardt proved the worst-case upper bound 2L / 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 20. 30897 K and 20. 10299 L, respectively. |