Abstract. In 1980 B. Monien and E. Speckenmeyer proved that satisfiability of a propositional formula consisting of K clauses can be checked in time of the order 2^K/3. Recently O. Kullmann and H. Luckhardt proved the bound 2^L/9, where L is the length of the input formula. The algorithms leading to these bounds (like many other SAT algorithms) are based on splitting, i.e. they reduce SAT for a formula F to SAT for several simpler formulas F₁, F₂, ... , F_m. These algorithms simplify each of F₁, F₂, ... , F_m. according to some transformation rules such as the elimination of pure literals, the unit propagation rule etc. In this paper we present a new transformation rule and two algorithms using this rule. These algorithms have the bounds 2^0.30897K and 2^0.10537L respectively.

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