Open this publication in new window or tab >>2005 (English)In: Theoretical Computer Science, ISSN 0304-3975, Vol. 332, no 1-3, p. 265-291Article in journal (Refereed) Published
Abstract [en]
We here present algorithms for counting models and max-weight models for 2SAT and 3SAT formulae. They use polynomial space and run in O(1.2561^{n}) and O(1.6737^{n}) time, respectively, where n is the number of variables. This is faster than the previously best algorithms for counting non-weighted models for 2SAT and 3SAT, which run in O(1.3247^{n}) and O(1.6894^{n}) time, respectively. In order to prove these time bounds, we develop new measures of formula complexity, allowing us to conveniently analyze the effects of certain factors with a large impact on the total running time. We also provide an algorithm for the restricted case of separable 2SAT formulae, with fast running times for well-studied input classes. For all three algorithms we present interesting applications, such as computing the permanent of sparse 0/1 matrices.
Keywords
Counting models; Satisfiability; Exponential-time algorithms; Exact algorithms; Upper bounds
National Category
Engineering and Technology
Identifiers
urn:nbn:se:liu:diva-14396 (URN)10.1016/j.tcs.2004.10.037 (DOI)
2007-04-162007-04-162017-02-23