Separating signs in the propositional satisfiability problem

Результат исследований: Научные публикации в периодических изданияхстатья

Аннотация

In 1980, Monien and Speckenmeyer and (independently) Dantsin proved that the satisfiability of a propositional formula in CNF can be checked in less than 2N steps (N is the number of variables). Later, many other upper bounds for SAT and its subproblems were proved. A formula in CNF is in CNF- (1, ∞) if each positive literal occurs in it at most once. In 1984, Luckhardt studied formulas in CNF-(1, ∞). In this paper, we prove several a new upper bounds for formulas in CNF-(l.∞) by introducing new signs separation principle. Namely, we present algorithms working in time of order 1.1939K and 1.0644L for a formula consisting of K clauses containing L literal occurrences. We also present an algorithm for formulas in CNF-(1, ∞) whose clauses are bounded in length.

Язык оригиналаанглийский
Страницы (с-по)442-463
Число страниц22
ЖурналJournal of Mathematical Sciences
Том98
Номер выпуска4
DOI
СостояниеОпубликовано - 1 янв 2000

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

  • Теория вероятности и статистика
  • Математика (все)
  • Прикладная математика

Fingerprint Подробные сведения о темах исследования «Separating signs in the propositional satisfiability problem». Вместе они формируют уникальный семантический отпечаток (fingerprint).

  • Цитировать