Abstract. In 1980 B. Monien and E. Speckenmeyer, and (independently) E. Ya. Dantsin proved that 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 we proved. A formula in CNF is in CNF-(1,\infty), if each positive literal occurs in it at most once. H. Luckhardt in 1984 studied formulas in CNF-(1,\infty). In this paper we prove several new upper bounds for formulas in CNF-(1,\infty) by introducing new signs separation principle. Namely, we present algorithms working the time of the order 1.1939K and 1.0644L for a formula consisting of K clauses containing L literals occurences. We also present an algorithm for formulas in CNF-(1,\infty) whose clauses are bounded in length.
Full text: [ .ps.gz in English (draft) (104 Kb) ] [ .ps.gz in Russian ]