New worst-case upper bounds for SAT. (English) Zbl 0960.03009

Hirsch, Edward A.

J. Autom. Reasoning 24, No. 4, 397-420 (2000).

Summary: 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.30897 K}\) and \(2^{0.10299L}\), respectively.

MSC:

03B35	Mechanization of proofs and logical operations
03D15	Complexity of computation (including implicit computational complexity)
68Q25	Analysis of algorithms and problem complexity

Keywords:

satisfiability of a propositional formula; transformation rule; algorithms; worst-case upper bounds