Is there a sometimes-efficient algorithm to solve #SAT?
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] Vilhelm Dahllöf, Peter Jonsson, and Magnus Wahlström. Counting Satisfying Assignments in 2-SAT and 3-SAT. In Proceedings of the 8th Annual International Computing and Combinatorics Conference (COCOON-2002), 535-543, 2002.

[2] W. Wei, and B. Selman. A New Approach to Model Counting. In Proceedings of SAT05: 8th International Conference on Theory and Applications of Satisfiability Testing, volume 3569 of Lecture Notes in Computer Science, 324-339, 2005.

[3] R. Gogate, and R. Dechter. Approximate Counting by Sampling the Backtrack-free Search Space. In Proceedings of AAAI-07: 22nd National Conference on Artificial Intelligence, 198–203, Vancouver, 2007.

[4] C. P. Gomes, J. Hoffmann, A. Sabharwal, and B. Selman. From Sampling to Model Counting. In Proceedings of IJCAI-07: 20th International Joint Conference on Artificial Intelligence, 2293–2299, 2007.

[5] L. Kroc, A. Sabharwal, and B. Selman. Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting. In CPAIOR-08: 5th International Conference on Integration of AI and OR Techniques in Constraint Programming, volume 5015 of Lecture Notes in Computer Science, 127–141, 2008.

[6] K. Kutzkov. New upper bound for the #3-SAT problem. Information Processing Letters 105(1), 1-5, 2007.