Minato ISOP 算法

Glossary

算法

Minato 算法的用途是寻找一个布尔函数的 素不可约覆盖 。换句话说：

• 我们希望找到一个原布尔函数的析取范式（Sum of Products）形式
• 其中每一个 合取项 都是 素蕴含项，即其中不包含任何可以删去的变量，或者说这个项是最小的
• 删除任何一个 合取项 都会使得这个 析取范式 不完整（不能表达原本的函数）。

我们来逐个解决。

析取范式

最简单的把任意布尔函数写成析取范式的方案是 香农展开，直接

• 固定一个变量的值为0，计算布尔函数的值
• 固定一个变量的值为1，计算布尔函数的值
• 通过 乘（合取）上这个变量或其取反 将结果合并

即，设有布尔函数 $f(x_0,\cdots, x_n)$，我们可以递归应用：

$$ f(x_0, x_1, \cdots, x_n) = \neg x_0 \cdot (f(0, x_1, \cdots, x_n)) + x_0 \cdot (f(1, x_1, \cdots, x_n)) $$

直至 $f$ 的参数完全是确定的为止。

这样展开得到的显然是一个覆盖，但是既不保证 素 也不保证 不可约。

素 与 不可约

我们在 香农展开 的基础上进行改进： 假设 $f$ 的 香农展开 的两个部分是 $f_0(x_1, \cdots, x_n) = f(0, x1, \cdots, x_n)$, $f_1(x_1, \cdots, x_n) = f(1, x1, \cdots, x_n)$。

如果一组 $x_1, \cdots, x_n$

• 在 $f_0$ 下为 1，但在 $f_1$ 下为 0，那么说明这组 $x$ 只有在 $x_0$ 为 0 才可能使得原函数为 1，即对应的项需要乘上一个 $\neg x_0$ 才能成为一个蕴含项。
• 在 $f_1$ 下为 1，但在 $f_0$ 下为 0，那么说明这组 $x$ 只有在 $x_0$ 为 1 才可能使得原函数为 1，即对应的项需要乘上一个 $x_0$ 才能成为一个蕴含项。
• 在 $f_0$ 下为 0，说明只要 $x_0$ 为 0，整个原函数就不可能为 1，即对应项不可以包含 $\neg x_0$，否则就不能成为一个蕴含项。
• 在 $f_1$ 下为 0，说明只要 $x_0$ 为 1，整个原函数就不可能为 1，即对应项不可以包含 $x_0$，否则就不能成为一个蕴含项。
• 在 $f_1$ 和 $f_0$ 下都为 1 的情况下，$x_0$ 不能影响 原函数 的值，这种情况下对应的项中不包含 $x_0$ 或是 $\neg x_0$

通过上面的分析，我们可以发现 除了 $f_0$ 和 $f_1$ 都为 1 的情况，别的三种情况都可以直接确定出所对应的一部分蕴含项了，当然，要获取到最终的结果，还需要递归地将 $f_1$ 和 $f_0$ 转换为素不可约覆盖。

而对于 $f_0$ 和 $f_1$ 都为 1 的情况，只需把 $x_0$ 抛弃，继续从 $x_1$ 部分开始判断即可。

按照这个流程得到的就是 素不可约覆盖。

高效实现

数据结构

我们用 BDD 表示逻辑公式。

对于找到的覆盖，虽然也可以用 BDD 表示，但更高效的表示方式是 零抑制决策图 （Zero-Suppressed Binary Decision Diagram, ZDD）。

零抑制决策图（Zero-Suppressed Binary Decision Diagram, ZDD）

ZDD 相比 BDD 更适合表示集合的集合，比如 一个逻辑表达式的覆盖 其中每个项都是一个集合，而其整体就是这些集合的集合。

使用 ZDD 表示 逻辑表达式的覆盖 的方法如下：

• 除了最底部的一层是两个特殊节点 $\{ \varnothing \}$（$\top$） 和 $\varnothing$（$\bot$）之外，每层表示一个原子变量或其否定 $\neg x$，因此对于 k 个原子变量的逻辑公式，最多需要 2k + 1 个层的 zdd 来表示
• 对每个位于表示原子变量 $x$ 或其否定 $\neg x$ 的层中的节点，其 low 分支表示不包含 $x$ 的集合，其 high 分支表示包含 $x$ 的集合。

更多关于 ZDD 的信息，见 。

算法

// `f`: 需要生成覆盖的 Boolean function
// `fd`: `f` 和 don't care set （可以覆盖也可以不覆盖）的 union
//   如果不存在 don't care set，直接输入两个 f 即可
fn irr_sop(f: BDD, fd: BDD) -> ZDD {
  if (f == BDD::Bottom) return {};
  if (fd == BDD::Top) return {{}};

  let f_top: BDDVariable = top_variable(f);
  let fd_top: BDDVariable = top_variable(fd);
  let x: BDDVariable = f_top < fd_top ? f_top : fd_top;

  let (f0, f1): (BDD, BDD) = decompose_bdd(f, x);
  let (fd0, fd1): (BDD, BDD) = decompose_bdd(fd, x);

  // g0: 必须 由 包含 !x 的项覆盖的部分
  let g0: BDD = f0 - fd1;
  let r0: ZDD = irr_sop(g0, fd0);

  // g1: 必须 由 包含 x 的项覆盖的部分
  let g1: BDD = f1 - fd0;
  let r1: ZDD = irr_sop(g1, fd1);

  // h: 没有成功被 r0 和 r1 覆盖掉的部分
  let h: BDD = (f0 - BDD(r0)) + (f1 - BDD(r1));
  let hd: BDD = fd0 & fd1;
  let r2: ZDD = irr_sop(h, hd);

  !x・r0 + x・r1 + r2
}

其中 $f - g = f \cdot (\neg g)$

例子

假设有如下函数（用真值表表示）：

直接把最小项拿出来，可以得到最简单的函数表示：

$$ \neg A \neg B C + \neg A B \neg C + A \neg B \neg C + A B \neg C $$

将其带入 f 和 fd：

• $x = A$
• $f_0 = fd_0 = \neg B C + B \neg C$
• $f_1 = fd_1 = \neg B \neg C + B \neg C$
• $g_0 = f_0 - fd_1 = (\neg B C + B \neg C) \cdot \neg (\neg B \neg C + B \neg C) = \neg BC$
• $g_1 = f_1 - fd_0 = (\neg B \neg C + B \neg C) \cdot \neg (\neg B C + B \neg C) = \neg B \neg C$
• 递归计算 r_0 = irr_sop(g_0, fd_0) = irr_sop(!B・C, !B・C + B・!C)
  • $x = B$
  • $f_0 = C$
  • $fd_0 = C$
  • $f_1 = 0$
  • $fd_1 = \neg C$
  • $g_0 = f_0 - fd_1 = C \cdot \neg (\neg C) = C$
  • $g_1 = f_1 - fd_0 = 0$
  • 递归计算 r_0 = irr_sop(g_0, fd_0) = irr_sop(C, C)
    • $x = C$
    • $f_0 = fd_0 = 0$
    • $f_1 = fd_1 = 1$
    • $g_0 = f_0 - fd_1 = 0$
    • $g_1 = f_1 - fd_0 = 1$
    • 递归计算 r_0 = irr_sop(g_0, fd_0) = irr_sop(0, 0) = 0。
    • 递归计算 r_1 = irr_sop(g_1, fd_1) = irr_sop(1, 1) = 1。
    • $h = 0 \cdot \neg 0 + 1 \cdot \neg 1 = 0$
    • $hd = 0 \cdot 1 = 0$
    • 递归计算 r_2 = irr_sop(h, hd) = irr_sop(0, 0) = 0。
    • 返回 $r_0 = \neg C・0 + C・1 + 0 = C$
  • 递归计算 r_1 = irr_sop(g_1, fd_1) = irr_sop(0, !C) = 0
  • $h = C \cdot \neg C + 0 \cdot \neg 0 = 0$
  • $hd = C \cdot \neg C = 0$
  • 递归计算 r_2 = irr_sop(h, hd) = irr_sop(0, 0) = 0。
  • 返回 $r_0 = \neg B・C + B・0 + 0 = \neg BC$
• 递归计算 r_1 = irr_sop(g_1, fd_1) = irr_sop(!B・!C, !B・!C + B・!C)
  • $x = B$
  • $f_0 = \neg C$
  • $fd_0 = \neg C$
  • $f_1 = 0$
  • $fd_1 = \neg C$
  • $g_0 = f_0 - fd_1 = \neg C \cdot \neg (\neg C) = 0$
  • $g_1 = f_1 - fd_0 = 0 \cdot \neg (\neg C) = 0$
    • 递归计算 r_0 = irr_sop(g_0, fd_0) = irr_sop(0, !C) = 0
    • 递归计算 r_1 = irr_sop(g_1, fd_1) = irr_sop(0, !C) = 0
    • $h = (\neg C - 0) + (0 - 0) = \neg C$
    • $hd = \neg C$
    • 递归计算 r_2 = irr_sop(h, hd) = irr_sop(!C, !C) = !C
    • 返回 $r_1 = \neg B \cdot 0 + B \cdot 0 + \neg C = \neg C$
• $h = (\neg B C + B \neg C - \neg BC) + (\neg B \neg C + B \neg C - \neg C) = B \neg C$
• $hd = (\neg B C + B \neg C) \cdot (\neg B \neg C + B \neg C) = B \neg C$
• 递归计算 r_2 = irr_sop(h, hd) = irr_sop(B・!C, B・!C) = B・!C。
• 返回最终结果 $\neg A \neg B C + A \neg C + B \neg C$