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
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.
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).
dragontamer|3 years ago
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|3 years ago