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