There are

  • $k$ Boolean variables $x_1, x_2, \dots, x_k$.

  • $m$ arbitrary subsets of these variables such that sum of each set equals to $1$ (i.e., only one variable is $1$, the others are $0$). E.g., one of $m$ constraints may be $x_1 + x_3 + x_5 + x_6 = 1$.

  • $n$ arbitrary subsets of these variables such that sum of each set is at least $1$ (i.e., at least one of the variables should be $1$). E.g., one of $n$ constraints may be $x_1 + x_6 + x_8 \geq 1$.

The solutions are not necessary, but I want to know how many solutions exist.

What is an efficient way to calculate the number of solutions?


There is unlikely to be any efficient algorithm.

Your first class of constraints are monotone exactly-1 CNF clauses. Your second class of constraints are monotone CNF clauses. The monotone part indicates that negated literals aren't allowed (you can't have $x_1 - x_3 = 1$ or $x_1 - x_4 \ge 1$).

Thus, in the special case where you have only type-2 constraints, the problem becomes #monotone-SAT. Unfortunately, this problem is known to be hard. #SAT is #P-complete, and monotone #SAT is #P-complete as well: it is #P-complete even for monotone 2CNF clauses (i.e., type-2 constraints with only two variables). It is also known that it is NP-hard to approximate the number of solutions. As a result, there is unlikely to be any efficient solution unless the number of variables and constraints is fairly small. Of course, your problem (with a mixture of type-1 and type-2 constraints) is potentially even harder.

So what can you do, to make the best of the situation?

One approach is to code this as an instance of #SAT, and try applying some off-the-shelf #SAT solver. You can encode type-1 constraints in SAT using the methods described at Encoding 1-out-of-n constraint for SAT solvers.

Or, you could express the constraints as a BDD and then apply model-counting methods for BDDs. I expect this to perform worse than a #SAT solver, but you could try it.

Another approach is to use an approximation algorithm. There are existing algorithms for approximate-#SAT, though they too will hit a limit if you have too many variables and/or clauses.

  • $\begingroup$ His ​ "second class of constraints are" ​ monotone CNF clauses. ​ ​ ​ ​ $\endgroup$ – user12859 May 12 '17 at 22:57
  • $\begingroup$ @RickyDemer, Oh! You are absolutely right -- I missed that negative literals aren't allowed. I've edited the answer accordingly -- thank you! $\endgroup$ – D.W. May 13 '17 at 0:32
  • 1
    $\begingroup$ The negation of x can easily encoded with x+y=1. Then y is the negation of x. $\endgroup$ – Albert Hendriks May 13 '17 at 7:01
  • 1
    $\begingroup$ Nice answer. One extra point is that Exact Cover can be straightforwardly encoded using only type-1 constraints (basically, for each ground set element, make an exactly-1 constraint listing the sets that contain this element), which means that it's NP-hard to even decide whether there are any solutions to this problem (in fact, to the special cases consisting of only type-1 constraints). $\endgroup$ – j_random_hacker May 13 '17 at 8:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.