An algorithm for the SAT problem for formulae of linear length

We present an algorithm that decides the satisfiability of a CNF formula where every variable occurs at most h times in time O(2(N(1-c/(k+1)+O(1/k2)))) for some c (that is, O(alpha(N)) with alpha < 2 for every fixed k). For k <= 4, the results coincide with an earlier paper where we achieved running times of O(2(0.1731N)) for k = 3 and O(2(0.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(2(0.4629N)) for k = 5 and O(2(0.5408N)) for k = 6. As a consequence of this, the same algorithm is shown to run in time O(2(0.926L)) for a formula of length (i.e. total number of literals) L. The previously best bound in terms of L is O(2(0.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.