Counting models for 2SAT and 3SAT formulae

• DOI: 10.1016/j.tcs.2004.10.037
• Publication Date: 2004-11-18T01:37:05Z
• Authors: Vilhelm Dahllöf; Peter Jonsson; Magnus Wahlström
• Keywords: Boolean satisfiability problem; Satisfiability

AbstractWe here present algorithms for counting models and max-weight models for 2SAT and 3SAT formulae. They use polynomial space and run in O(1.2561n) and O(1.6737n) 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.3247n) and O(1.6894n) 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.