I would just feed this to a counting SAT, or constraint, solver.

If I wrote the constraint solver, does that count as an acceptable answer?

There are some fancy ways of doing this, involving lots of bitshifting, which are quite fun.

Edit: Remove mis-remembered bitshifting.