[fcholf]

This is not the same goal as SAT. SAT looks for one satisfying assignment while OBDD tries to represent the full set of satisfying assignment in a factorized way to be analyzed later. For example, trying to count the number of satisfying assignment using a vanilla SAT-solver would be quite bad as you would end up generating every assignment while OBDD can sometimes take advantage of factorizing some part of the input.

But even if you are only interested in satisfiability, it sometimes happened that OBDD-based solvers are more efficient than CDCL SAT-solver. Indeed, for some application, you need to have richer constraints than the clauses used in CNF formulas. For example, for circuit synthesis, you often need to represent parity constraints (parity(x1...xn) is true iff there are an even number of values set to 1). CNF encoding of such constraints are expensive and kill most of the clever stuff that CDCL solvers do, while representing a parity constraint is actually quite easy with an OBDD of size 2n.

[freemint]

There are also sat solvers which do (approximate) solution counting. It is just that all these pointers seems so cache unfriendly ... But thank you for your insight

[dragontamer]

See the paper "The Number of Knight's Tours Equals 33,439,123,484,294 | Counting with Binary Decision Diagrams" by Martin Lobbing and Ingo Wegener. Bonus points, this occurred in the 80s, when computers only had kilobytes of memory (not even MBs). So... yeah, BDDs are an incredibly powerful technique.

BDDs obtain an exact count, and are among the most efficient algorithms for this problem.

"Counting" the solutions is closely related to "finding at least one solution". But they are fundamentally different. BDDs will be "less efficient at finding just one solution" compared to traditional SAT solvers. But SAT solvers are much less efficient at enumerating the entire solution space and/or finding exact counts.

[fcholf]

I would be curious to know examples of SAT solvers you have in mind for approximate counting. The only tools I am aware of for approximate counting are dedicated to this task (and usually use SAT solvers as oracles under the hood).