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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Wahlström, M. (2005). Faster exact solving of SAT formulae with a low number of occurrences per variable. In Lecture Notes in Computer Science (Vol. 3569, pp. 309–323). Springer Verlag. https://doi.org/10.1007/11499107_23
Mendeley helps you to discover research relevant for your work.