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 2^N 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.1939^K and 1.0644^L 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.