Efficient algorithm for simple constraint satisfaction problem

Question

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?

Answer 1

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.

• user12859: His ​ "second class of constraints are" ​ monotone CNF clauses. ​ ​ ​ ​
• D.W.: @RickyDemer, Oh! You are absolutely right -- I missed that negative literals aren't allowed. I've edited the answer accordingly -- thank you!
• Albert Hendriks: The negation of x can easily encoded with x+y=1. Then y is the negation of x.
• j_random_hacker: 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).