Problem
How do you write a "product-of-sums" Boolean expression, in m Boolean variables, which enforces at least n of those variables being 1/true?
Attempt
Starting in the "sum-of-products" form, my solution is as follows for the specific example of n = 3 and m = 4 (A, B, C, D):
(A and B and C) or (A and B and D) or (A and C and D) or (B and C and D)
The above expression is a mathematical combination (without replacement, order irrelevant) of every 3 variables out of the 4. In other words, it lists all the possibilities of 3 or more variables out of the 4 being logically high. As such, there are 4 or-separated (parenthesized) groups with 3 and-separated variables per group.
However, a software tool that I am using does not accept this format. I need to convert from the above expression's sum-of-products form of Boolean expression to the product-of-sums form, which is as follows:
(A or B) and (A or C) and (A or D) and (B or C) and (B or D) and (C or D)
Note that there are now 6 and-separated (parenthesized) groups with 2 or-separated variables per group. Though part of my attempted solution, I haven't been able to find a relationship between the number of groups and the number of variables per group between the sum-of-products form and the product-of-sums form. I would like to generalize the above solution for an arbitrary n, up to n = 10, and an arbitrary m, up to m = 24.
So, the problem may be re-phrased as follows: How do I convert from a sum-of-products expression, of all combinations of n out of m variables being logically high, to the corresponding product-of-sums expression? The solution ought to be generalized for an arbitrary (n, m) and not rely on CAS-type tools like this which do not scale well to large problems. I am using Python and have looked at libraries like pyeda, whose conversions to long product-of-sums expressions seem to be very computationally expensive.
The Boolean n-of-m expression can be encoded as products-of-sums in several ways. A recommended paper is Towards an Optimal CNF Encoding of
Boolean Cardinality Constraints of Carsten Sinz.
Basically, the encoding makes use of a combination of digital counter and digital comparator. The counter evaluates the number of variables equal to true. The comparator determines, if the resulting number ends up within the allowed range. The paper explains how to derive the Conjunctive Normal Form (CNF), the usual name for products-of-sums form.
In case you are not willing to implement such a solution yourself, you could resort to bc2cnf. This is a small versatile tool, which is able (among other things) to convert n-of-m cardinality constraints to CNF in DIMACS format.
Input for an at-least-10-of-24 example:
BC1.0
// at least 10 of 24
_x := [10,24](a,b,c,d,e,f,g,h,i,j,k,l,m,n,p,q,r,s,t,u,v,w,x);
ASSIGN _x;
The resulting CNF is generated in fractions of a second. It has 460 clauses.
Make sure to use the -all parameter. Otherwise, you'll just get a CNF to check for general satisfiability.
A Python implementation of cardinality encodings is provided by PySAT. pysat.card encodes cardinality constraints into a CNF formula.