TY - JOUR

T1 - Separating signs in the propositional satisfiability problem

AU - Hirsch, E. A.

PY - 2000/1/1

Y1 - 2000/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=52849120789&partnerID=8YFLogxK

U2 - 10.1007/BF02362266

DO - 10.1007/BF02362266

M3 - Article

AN - SCOPUS:52849120789

VL - 98

SP - 442

EP - 463

JO - Journal of Mathematical Sciences

JF - Journal of Mathematical Sciences

SN - 1072-3374

IS - 4

ER -