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/k~2))) 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(2~(0.1736N)) 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.0926L)) 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.
展开▼
