Proceedings of SODA'98, pp.521-530.

**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_{1}, F_{2}, ... , F_{m}.
These algorithms simplify each of
F_{1}, F_{2}, ... , 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) ]

Back to the list of papers