[mcint]

Well, at this scale, it would take longer to set up a SAT solver than it would for the SAT solver to list all valid solutions.