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

Question

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?

Answer 1

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.

Answer 2

In addition to the papers listed by Juho, here are some others that describe work on this topic, especially on approximating the number of solutions:

• Model Counting. Carla P. Gomes, Ashish Sabharwal, Bart Selman Handbook of Satisfiability, IOS Press. Editors: Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh. Chapter 20, pp 633-654, 2009.

  • This has a nice overview of the topic and introduction to a number of techniques.

• Near-Uniform Sampling of Combinatorial Spaces Using XOR Constraints. Carla P. Gomes, Ashish Sabharwal, Bart Selman. NIPS-06. 20th Annual Conference on Neural Information Processing Systems, pp 481-488, Vancouver, BC, Canada, Dec 2006.

• Short XORs for Model Counting: From Theory to Practice. Carla P. Gomes, Joerg Hoffmann, Ashish Sabharwal, Bart Selman SAT-07. 10th International Conference on Theory and Applications of Satisfiability Testing, LNCS volume 4501, pp 100-106, Lisbon, Portugal, May 2007.

• Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting. Lukas Kroc, Ashish Sabharwal, Bart Selman ANOR-2011. Annals of Operations Research, volume 184, number 1, pp 209-231, 2011.

• Heuristics for Fast Exact Model Counting. Tian Sang, Paul Beame, and Henry Kautz. Theory and Applications of Satisfiability Testing (SAT 2005), pp 226-240.