4
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ His ​ "second class of constraints are" ​ monotone CNF clauses. ​ ​ ​ ​ $\endgroup$
    – user12859
    May 12, 2017 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, 2017 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, 2017 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, 2017 at 8:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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