Is there a sometimes-efficient algorithm to solve #SAT?

Let $B$ be a boolean formula consisting of the usual AND, OR, and NOT operators and some variables. I would like to count the number of satisfying assignments for $B$. That is, I want to find the number of different assignments of truth values to the variables of $B$ for which $B$ assumes a true value. For example, the formula $a\lor b$ has three satisfying assignments; $(a\lor b)\land(c\lor\lnot b)$ has four. This is the #SAT problem.

Obviously an efficient solution to this problem would imply an efficient solution to SAT, which is unlikely, and in fact this problem is #P-complete, and so may well be strictly harder than SAT. So I am not expecting a guaranteed-efficient solution.

But it is well-known that there are relatively few really difficult instances of SAT itself. (See for example Cheeseman 1991, "Where the really hard problems are".) Ordinary pruned search, although exponential in the worst case, can solve many instances efficiently; resolution methods, although exponential in the worst case, are even more efficient in practice.

My question is:

Are any algorithms known which can quickly count the number of satisfying assignments of a typical boolean formula, even if such algorithms require exponential time in the general instance? Is there anything noticeably better than enumerating every possible assignment?

-
I tried to add a tag for #p-completeness, but the Stack Exchange software doesn't like the # sign. –  Mark Dominus Jan 16 '13 at 0:24
I'd be careful with claiming that "there are relatively few really difficult instances of SAT itself". I believe the paper you link actually talks about random $k$-SAT. Furthermore, the phase transition phenomenon only applies to the random instances. There are many really tough handcrafted, industrial etc. instances of SAT. –  Juho Jan 16 '13 at 0:32
Thanks. Do you think this tends to make my question less clear? Do you understand what I am asking for? –  Mark Dominus Jan 16 '13 at 0:35
It is clear to me. It's only important to remember what instances exhibit the phase transition :) –  Juho Jan 16 '13 at 0:42

Counting in the general case

The problem you are interested in is known as #SAT, or model counting. In a sense, it is the classical #P-complete problem. Model counting is hard, even for $2$-SAT! Not surprisingly, the exact methods can only handle instances with around hundreds of variables. Approximate methods exist too, and they might be able to handle instances with around 1000 variables.

Exact counting methods are often based on DPLL-style exhaustive search or some sort of knowledge compilation. The approximate methods are usually categorized as methods that give fast estimates without any guarantees and methods that provide lower or upper bounds with a correctness guarantee. There are also other methods that might not fit the categories, such as discovering backdoors, or methods that insist on certain structural properties to hold on the formulas (or their constraint graph).

There are practical implementations out there. Some exact model counters are CDP, Relsat, Cachet, sharpSAT, and c2d. The sort of main techniques used by the exact solvers are partial counts, component analysis (of the underying constraint graph), formula and component caching, and smart reasoning at each node. Another method based on knowledge compilation converts the input CNF formula into another logical form. From this form, the model count can be deduced easily (polynomial time in the size of the newly produced formula). For example, one might convert the formula to a binary decision diagram (BDD). One could then traverse the BDD from the "1" leaf back to the root. Or for another example, the c2d employs a compiler that turns CNF formulas into deterministic decomposable negation normal form (d-DNNF).

If your instances get larger or you don't care about being exact, approximate methods exist too. With approximate methods, we care about and consider the quality of the estimate and the correctness confidence associated with the estimate reported by our algorithm. One approach by Wei and Selman [2] uses MCMC sampling to compute an approximation of the true model count for the input formula. The method is based on the fact that if one can sample (near-)uniformly from the set of solution of a formula $\phi$, then one can compute a good estimate of the number of solutions of $\phi$.

Gogate and Dechter [3] use a model counting technique known as SampleMinisat. It's based on sampling from the backtrack-free search space of a boolean formula. The technique builds on the idea of importance re-sampling, using DPLL-based SAT solvers to construct the backtrack-free search space. This might be done either completely or up to an approximation. Sampling for estimates with guarantees is also possible. Building on [2], Gomes et al. [4] showed that using sampling with a modified randomized strategy, one can get provable lower bounds on the total model count with high probabilistic correctness guarantees.

There is also work that builds on belief propagation (BP). See Kroc et al. [5] and the BPCount they introduce. In the same paper, the authors give a second method called MiniCount, for providing upper bounds on the model count. There's also a statistical framework which allows one to compute upper bounds under certain statistical assumptions.

Algorithms for #2-SAT and #3-SAT

If you restrict your attention to #2-SAT or #3-SAT, there are algorithms that run in $O(1.3247^n)$ and $O(1.6894^n)$ for these problems respectively [1]. There are slight improvements for these algorithms. For example, Kutzkov [6] improved upon the upper bound of [1] for #3-SAT with an algorithm running in time $O(1.6423^n)$.

As is in the nature of the problem, if you want to solve instances in practice, a lot depends on the size and structure of your instances. The more you know, the more capable you are in choosing the right method.

-
+1 Nice answer. –  Kaveh Jan 21 '13 at 9:05