An algorithm for the SAT problem for formulae of linear length

Abstract

We present an algorithm that decides the satisfiability of a CNF formula where every variable occurs at most k times in time O(2 N(1-c/(k+1)+O(1/k2))) for some c (that is, O(αN) with α < 2 for every fixed k). For k ≤ 4, the results coincide with an earlier paper where we achieved running times of O(20.1736N) for k = 3 and O(20.3472N) for k = 4 (for k ≤ 2, the problem is solvable in polynomial time). For k > 4, these results are the best yet, with running times of O(20.4629N) for k = 5 and O(20.5408N) for k = 6. As a consequence of this, the same algorithm is shown to run in time O(2 0.0926L) for a formula of length (i.e. total number of literals) L. The previously best bound in terms of L is O(20.1030L). Our bound is also the best upper bound for an exact algorithm for a 3SAT formula with up to six occurrences per variable, and a 4SAT formula with up to eight occurrences per variable. © Springer-Verlag Berlin Heidelberg 2005.