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
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.