An algorithm for the sat problem for formulae of linear length
2005 (English)In: Algorithms – ESA 2005: 13th Annual European Symposium, Palma de Mallorca, Spain, October 3-6, 2005., 2005, 107 -118 p.Conference paper (Other academic)
We present an algorithm that decides the satisfiability of a CNF formula where every variable occurs at most k times in time for some c (that is, O(αN) with for every fixed k). For k ≤ 4, the results coincide with an earlier paper where we achieved running times of O(20.1736N) for k = 3 and O(20.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(20.4629N) for k = 5 and O(20.5408N) for k = 6. As a consequence of this, the same algorithm is shown to run in time O(20.0926L) for a formula of length (total number of literals) L. The previously best bound in terms of L is O(20.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.
Place, publisher, year, edition, pages
2005. 107 -118 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 (Print) 1611-3349 (Online) ; 3669
Engineering and Technology
IdentifiersURN: urn:nbn:se:liu:diva-14398DOI: 10.1007/11561071ISBN: 978-3-540-29118-3OAI: oai:DiVA.org:liu-14398DiVA: diva2:23419