algorithm - boolean 函数密度的计算算法

Question

我正试图编写一个程序，需要计算一个处理布尔函数的特定值。给定一个输出布尔函数f，由一个覆盖f给出，假设我把函数的密度定义为函数值为1的所有输入向量的分数。
例如，假设我传入给定的函数f（a，b，c），该函数由覆盖层f=ab'+c'定义该函数有5个ON-set minterms和8个total minterms，因此其密度为d（f）=5/8=0.625需要注意的是，cube ab'包含2分钟，cube c'包含4分钟，但其中一分钟包含在两个立方体中。
有人能想出一个好的算法来处理这个问题吗我强烈怀疑它最好递归地表达，但是我很难确定什么是有效的。

Answer 1

坏消息是：不可能有一个总是很快的算法。
也就是说，这个问题：
给定一个合取范式（和的乘积）的布尔公式，决定是否有一个自由变量的赋值，使得公式产生真值。
是NP完全的。这意味着，如果你找到一个多项式时间算法来解决它，你也可以在多项式时间内解决一些世界上最困难的问题（背包问题、旅行推销员问题、哈密顿循环问题等等）。没有人真的期望这是可能的。
实际上，这个问题相当于这个问题：
给定一个析取范式的布尔公式（积和），决定其密度是否为100%
好消息是：
输入大小可能非常小。在三个变量下，你并不真正在乎速度在30个输入变量的情况下，您仍然可能会耗尽内存（使用一些算法），而不是运行太长。
算法1：O(2^v*i)时间，几行代码，v=变量数；i=输入长度。
如果任何子句不一致（A & !A），则删除它。
先按大小、最大值（变量最少）对子句进行排序。
对于通用集合中的每一个minterm
对于输入中的每个子句
对于术语中的每一个文字
如果文本不包含minterm，请继续下一个子句
本条款包括以下条款：
将minterm计算为已覆盖，然后继续下一个minterm。
minterm不包含在任何文本中；请继续下一个minterm。
设density = [#covered terms]/[#terms]
如果你想跑得更快，你需要一个良好的输入希望。您可以尝试使用二进制决策图（bdd）对当前编码的minterm集进行编码，并在从输入添加子句时尝试更新二进制决策图。
二元决策图是有根有向无环图，这样每个节点要么是决策节点（测试单个变量，然后获取假分支或真分支）要么是叶节点（要么true要么false）。例如，XOR可以用这个二元决策图来表示：

     |
     A
    / \
   /   \
  B     B
 / \   / \
0   1 1   0

算法2（延迟扩展bdd，对于大量变量来说更复杂但可能更快）：
如果任何子句不一致（ A & !A），则删除它。
先按大小、最大值（变量最少）对子句进行排序。
从空bdd开始（根=false）
每一个条款
更新BDD：从根目录开始。
对于每个变量：
如果子句没有更多的文本，请将当前节点替换为 true（仅在您所在的边缘）
如果直接同级也是 true，则将公共父级替换为 true，并对新节点重复此测试。
如果当前节点 true
继续下一个子句或递归分支，或加入同级线程。
如果变量在子句和当前bdd节点中，
转到与子句相交的子语句。
如果变量在子句中，但不在当前BDD节点中。
创建新的bdd节点
将两个子节点都设置为当前节点
将当前节点替换为新节点（仅在您到达的边缘）
转到与子句相交的子语句。
如果变量在bdd中，但不在子句中
依次递归下降到两个孩子。或者，以单独的线程并行下降到两个孩子。
如果变量既不在bdd中也不在子句中
什么都不做。
设 density = 0/(2^variables)（分母表示整数计算的建议比例）
每个叶节点要么 true要么 false对于bdd中的每一条路径
如果叶节点 true
设 length为沿路径遇到的非叶节点数。
将 1/(2^length)添加到 density。