Separating signs in the propositional satisfiability problem

Research output

Abstract

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.

Original languageEnglish
Pages (from-to)442-463
Number of pages22
JournalJournal of Mathematical Sciences
Volume98
Issue number4
DOIs
Publication statusPublished - 1 Jan 2000

Scopus subject areas

  • Statistics and Probability
  • Mathematics(all)
  • Applied Mathematics

Fingerprint Dive into the research topics of 'Separating signs in the propositional satisfiability problem'. Together they form a unique fingerprint.

  • Cite this