m个总变量中具有n个真变量的广义和乘积布尔表达式-解网

问：

问题

你如何在 m 个布尔变量中编写一个“求和的乘积”布尔表达式，它强制这些变量中至少有 n 个是 1/true？

尝试

从“乘积总和”形式开始，对于 n = 3 和 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)

上面的表达式是 4 个变量中每 3 个变量的数学组合（没有替换，顺序无关）。换句话说，它列出了 4 个变量中 3 个或更多变量在逻辑上很高的所有可能性。因此，有 4 个 or 分隔（括号内）组，每组有 3 个分隔变量。

但是，我正在使用的软件工具不接受这种格式。我需要将上面表达式的布尔表达式的乘积形式转换为求和的乘积形式，如下所示：

(A or B) and (A or C) and (A or D) and (B or C) and (B or D) and (C or D)

请注意，现在有 6 个 and 分隔（括号内）组，每个组有 2 个 or 分隔变量。虽然是我尝试的解决方案的一部分，但我无法在乘积表单和乘积表单之间找到组数和每组变量数之间的关系。我想将上述解决方案推广为任意 n（最多 n = 10）和任意 m（最多 m = 24）。

因此，问题可以重新表述如下：如何从乘积和表达式（m 个变量中 n 个变量中的所有组合在逻辑上都很高）转换为相应的乘积求和表达式？解决方案应该针对任意（n， m）进行推广，而不是依赖像这样的 CAS 类型的工具，这些工具不能很好地扩展到大型问题。我正在使用 Python，并且查看了像 pyeda 这样的库，它们转换为长和乘积表达式似乎在计算上非常昂贵。

布尔组合 boolean-logic boolean-expression

基数约束

布尔表达式可以通过多种方式编码为求和的乘积。推荐的论文是 Towards an Optimal CNF Encoding of Carsten Sinz 的布尔基数约束。n-of-m

基本上，编码利用了数字计数器和数字比较器的组合。计数器计算等于 true 的变量数。比较器确定结果数字是否在允许的范围内。本文解释了如何推导结合正态形式（CNF），这是和积形式的通常名称。

转换器工具bc2cnf来救援

如果您不愿意自己实现这样的解决方案，您可以求助于 bc2cnf。这是一个小型的多功能工具，它能够（除其他外）将基数约束转换为 DIMACS 格式的 CNF。n-of-m

示例输入：at-least-10-of-24

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;

生成的 CNF 在几分之一秒内生成。它有 460 个子句。

请确保使用该参数。否则，你只会得到一个 CNF 来检查总体满意度。-all

Python 中的 CNF 基数编码

PySAT 提供了基数编码的 Python 实现。pysat.card 将基数约束编码为 CNF 公式。

m个总变量中具有n个真变量的广义和乘积布尔表达式

Generalized product-of-sums Boolean expression with n true variables out of m total variables

评论

基数约束

转换器工具bc2cnf来救援

Python 中的 CNF 基数编码

评论