I'm surprised not to see any mention of satisfiability here. There are a few papers I've seen about it, but this blog post seems to give a reasonable overview:

https://codingnest.com/modern-sat-solvers-fast-neat-underuse...

Then you just need to start counting models, which is the #SAT (sharp SAT) problem:

https://en.wikipedia.org/wiki/Sharp-SAT

Using software such as:

https://github.com/marcthurley/sharpSAT