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 2K/3. Recently O. Kullmann and H. Luckhardt proved the bound 2L/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 F1, F2, ..., Fm. These algorithms simplify each of F1, F2, ..., Fm 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 20.30897 K and 20.10537 L respectively.

Original languageEnglish
Pages521-530
Number of pages10
Publication statusPublished - 1 Dec 1998
EventProceedings of the 1998 9th Annual ACM SIAM Symposium on Discrete Algorithms - San Francisco, CA, USA
Duration: 25 Jan 199827 Jan 1998

Conference

ConferenceProceedings of the 1998 9th Annual ACM SIAM Symposium on Discrete Algorithms
CitySan Francisco, CA, USA
Period25/01/9827/01/98

Scopus subject areas

  • Software
  • Mathematics(all)

Fingerprint Dive into the research topics of 'Two new upper bounds for SAT'. Together they form a unique fingerprint.

  • Cite this

    Hirsch, E. A. (1998). Two new upper bounds for SAT. 521-530. Paper presented at Proceedings of the 1998 9th Annual ACM SIAM Symposium on Discrete Algorithms, San Francisco, CA, USA, .