Zapiski nauchnyh seminarov POMI No.241, 1997, pp.30-71.

English translation: Journal of Mathematical Sciences, Vol.98, No.4, 2000, pp.442-463.

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

Back to the list of papers