Separating sings in the propositional satisfiability problem

E. A. Hirsch

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part X, Tome 241 (1997), pp. 30-71

Résumé

In 1980 B. Monien and E. Speckenmeyer, and (independently) 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.