zbMATH — the first resource for mathematics

New worst-case upper bounds for SAT. (English) Zbl 0960.03009
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.

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