We present an algorithm that decides the satisfiability of a formula F on CNF form in time O(1.1279~((d-2)n)), if F has at most d occurrences per variable or if F has an average of d occurrences per variable and no variable occurs only once. For d ≤ 4, this is better than previous results. This is the first published algorithm that is explicitly constructed to be efficient for cases with a low number of occurrences per variable. Previous algorithms that are applicable to this case exist, but as these are designed for other (more general, or simply different) cases, their performance guarantees for this case are weaker.
展开▼
