Hirsch, E. A., New Worst-Case Upper Bounds for SAT.
Journal of Automated Reasoning (2nd special issue on SAT) 24(4): 397-420, 2000.
Also published in the book "Highlights of Satisfiability Research in the Year 2000",
Volume 63 in Frontiers in Artificial Intelligence and Applications, IOS Press, 2000.

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.30897K and 20.10299L respectively.

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

Back to the list of papers