Hirsch, E. A., Separating sings in the propositional satisfiability problem.
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 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 ]

Back to the list of papers