Faster exact solving of SAT formulae with a low number of occurrences per variable
2005 (English)In: Theory and Applications of Satisfiability Testing, 8th International Conference, SAT 2005, 2005, 309-323 p.Conference paper (Other academic)
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.
Place, publisher, year, edition, pages
2005. 309-323 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 (Print) 1611-3349 (Online) ; 3569
Engineering and Technology
IdentifiersURN: urn:nbn:se:liu:diva-14397DOI: 10.1007/11499107_23ISBN: 978-3-540-26276-3OAI: oai:DiVA.org:liu-14397DiVA: diva2:23418