Two new upper bounds for SAT

Результат исследований: Материалы конференцийматериалы

22 Цитирования (Scopus)

Аннотация

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.

Язык оригиналаанглийский
Страницы521-530
Число страниц10
СостояниеОпубликовано - 1 дек 1998
СобытиеProceedings of the 1998 9th Annual ACM SIAM Symposium on Discrete Algorithms - San Francisco, CA, USA
Продолжительность: 25 янв 199827 янв 1998

Конференция

КонференцияProceedings of the 1998 9th Annual ACM SIAM Symposium on Discrete Algorithms
ГородSan Francisco, CA, USA
Период25/01/9827/01/98

Предметные области Scopus

  • Программный продукт
  • Математика (все)

Fingerprint Подробные сведения о темах исследования «Two new upper bounds for SAT». Вместе они формируют уникальный семантический отпечаток (fingerprint).

  • Цитировать

    Hirsch, E. A. (1998). Two new upper bounds for SAT. 521-530. Документ представлен на Proceedings of the 1998 9th Annual ACM SIAM Symposium on Discrete Algorithms, San Francisco, CA, USA, .