In case others aren't familiar with the termiology: #SAT is the counting version of the SAT problem, which tries to find how many different solutions exist to a set of constraints)