零抑制 BDD 的交集——使用 ZDD 实现多项式

Question

我正在尝试使用 ZDD 实现单变量多项式，正如 other question 中的评论中所建议的那样。

我看过S. Minato的论文（你可以下载here），但是我不明白如何在这些ZDD上实现操作。

论文中的想法是多项式可以使用x^(2^i) 作为变量来表示。例如，x^5 + x^3 + x 可以重写为 x^4x^1 + x^2x^1 + x^1，如果您为每个 x^(2^i) 变量创建节点并与相乘的“1-edge”变量和相加的“0-edge”变量连接您可以轻松获得表示该多项式的图形。 ZDD 是在图上强制执行某些条件的此类图（有关更多信息，请阅读 Minato 的文章和维基百科关于 BDD 的 page）

系数可以类似地使用 2 的幂和来表示（例如 5 = 2^2 + 2^0 等。每个 2^i 都是一个变量，并且节点以相同的方式与 1 和 0 边连接）。

现在，我的问题是添加两个 ZDD 的算法。 算法看起来很简单：

如果 F 和 G (ZDD) 没有公共组合，则加法 (F + G) 可以是 只需合并它们即可完成。当它们包含一些常见的 组合，我们计算以下公式： (F + G) = S + (Cx2)， 其中 C = F ∩ G, S = (F U G) \ C 。通过重复这个过程， 常见的组合最终用尽，程序是 完成。

问题是：如何有效地找到“C”和“S”？

作者提供了乘法的代码，但是一旦你实现了前面的算法，代码实际上是微不足道的。而且由于没有提供这些算法，因此乘法运算也是“无用的”。

“合并”ZDD 的概念也没有得到很好的解释，尽管考虑到变量的顺序应该是一致的，只有一种方法可以将图合并在一起，以及保持这种顺序的规则可能很简单（我还没有将它们正式化，但我对它们有一个粗略的了解）。

Answer 1

这里的“合并”表示联合 (algorithm)。您也可以从示例中看到这一点：

4 * y     = { { 2^2, y } }
x         = { { x } }
4 * y + x = { { 2^2, y }, { x } }

这个想法是，内部集合代表产品，整个 ZDD 代表这些产品的总和，因此如果您只是在更多集合中进行 OR（也称为联合或合并），它们就会被有效地添加。

完整的求和算法实际上只是执行(A xor B) + 2 * (A and B)（递归），这相当于熟悉的按位加法算法，但xor 写为(A or B) without (A and B)。

这也很明显为什么在没有常见组合时简单地采用联合是可以的 - 如果 A and B 为空，A xor B 与 A or B 相同，并且“进位”为零。

OR、AND、XOR 和 BUTNOT 的算法在 The Art of Computer Programming 第 4 卷 section 7.1.4 中有详细解释（问题 199 的答案是相关的）。他们所有人的一般想法是，他们考虑两个子图，代表所有集合with变量v和所有集合没有变量@987654331 @ 分开（如果v 是一个或两个参数中的最顶层变量作为低和高子或输入本身，则两者都很容易找到），然后组合结果。

Union(F, G) =
  if (F = ∅) return G
  if (G = ∅) return F
  if (F = G) return F
  if (cache contains "F ∪ G" or "G ∪ F")
    return cached value

  if (F.v = G.v) result = MakeNode(F.v, F.lo ∪ G.lo, F.hi ∪ G.hi)
  if (F.v > G.v) result = MakeNode(G.v, F ∪ G.lo, G.hi)
  if (F.v < G.v) result = MakeNode(F.v, F.lo ∪ G, F.hi)

  cache result as "F ∪ G"
  return result

Intersect(F, G) =
  if (F = ∅ or G = ∅) return ∅
  if (F = G) return F
  if (cache contains "F ∩ G" or "G ∩ F")
    return cached value

  if (F.v = G.v) result = MakeNode(F.v, F.lo ∩ G.lo, F.hi ∩ G.hi)
  if (F.v > G.v) result = F ∩ G.lo
  if (F.v < G.v) result = F.lo ∩ G

  cache result as "F ∩ G"
  return result