计算布尔函数密度的算法

Question

我正在尝试编写一个程序，该程序需要计算处理布尔函数的特定值。给定一个单输出布尔函数 f，由覆盖 F 给出，假设我将函数的密度定义为函数值为 1 的所有输入向量的分数。

例如，假设我传入给定的函数 f(a, b, c)，它由 cover F = ab'+c' 定义。该函数有 5 个 ON-set minterms，总共 8 个 minterms，因此其密度为 d(f) = 5/8 = 0.625。应该注意的是，立方体 ab' 覆盖了 2 个最小项，立方体 c' 覆盖了 4 个最小项，但是这些最小项之一被两个立方体覆盖。

谁能想到一个好的算法来处理这个问题？我强烈怀疑最好以递归方式表达，但我无法确定有效的东西。

Answer 1

坏消息：永远快速的算法没有希望。

即，这个问题：

给定一个合取范式（和的乘积）的布尔公式，确定是否存在自由变量的赋值，使得公式产生真

是 NP 完全的。这意味着如果你找到一个多项式时间算法来解决它，你也可以在多项式时间内解决一些世界上最难的问题（背包问题、旅行商问题、哈密顿循环问题等等）。没有人真的期望这是可能的。

这个问题实际上等价于这个问题：

给定一个析取范式（乘积之和）的布尔公式，判断它的密度是否为 100%

好消息：

输入大小可能非常小。在三个变量中，您并不真正关心速度。在 30 个输入变量时，您仍然更有可能耗尽内存（使用某些算法），而不是运行时间长得无法忍受。

算法#1：O(2^v*i)时间，几行代码，v=变量数量；i=输入的长度。

• 如果任何子句不一致（A & !A），则将其删除。
• 按大小对子句进行排序，最大的（最少的变量）首先。
• 对于全集的每一个 minterm
  • 对于输入中的每个子句
    • 对于术语中的每个文字
      • 如果 minterm 未包含在字面上，则继续下一个子句
    • minterm 包含在以下条款中：
    • 将 minterm 计算为已覆盖，然后继续下一个 minterm。
  • minterm 没有被任何文字覆盖；继续下一个minterm。
• 让 density = [#covered terms]/[#terms]

如果你想跑得更快，你需要希望有一个好的输入。您可以尝试使用二元决策图 (BDD) 对当前编码的最小项集进行编码，并在从输入中添加子句时尝试更新二元决策图。

二进制决策图是一个根向无环图，使得每个节点是一个判决节点（测试单个可变，然后采取任一假分支或真分支）或叶节点（无论是true或false）。例如，XOR可以用这个二元决策图表示：

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

算法 #2（延迟扩展 BDD，更复杂但对于大量变量可能更快）：

• 如果任何子句不一致（A & !A），则将其删除。
• 按大小对子句进行排序，最大的（最少的变量）首先。
• 从一个空的 BDD 开始（root = false）
• 对于每个条款
  • 更新 BDD：从根开始。
  • 对于每个变量：
    • 如果该子句没有更多文字，则将当前节点替换为true（仅在您来到的边缘处）
      • 如果直接兄弟也是true，则用 替换共同的父true节点，并对新节点重复此测试。
    • 如果当前节点是 true
      • 继续下一个子句或递归分支，或加入同级线程。
    • 如果变量在子句中并且在当前 BDD 节点中，
      • 下降到与子句相交的子句。
    • 如果变量在子句中但不在当前 BDD 节点中。
      • 创建一个新的 BDD 节点
      • 将两个孩子都设置为当前节点
      • 用新节点替换当前节点（仅在您来的边缘）
      • 下降到与子句相交的子句。
    • 如果变量在 BDD 中但不在子句中
      • 依次递归下降到两个孩子。或者，在单独的线程中并行下降到两个孩子。
    • 如果变量既不在 BDD 中也不在子句中
      • 没做什么。
• 让density = 0/(2^variables)（分母表示整数计算的建议比例）
• 每个叶节点都是true或false。对于 BDD 中的每条路径
  • 如果叶节点是 true
    • 让length是沿路径遇到的非叶节点的数量。
    • 添加1/(2^length)到density.