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

Question

我正在尝试使用 ZDD 实现单变量多项式，如另一个问题的评论中所建议的。

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

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

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

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

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

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

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

此外，“合并”ZDD 的概念也没有得到很好的解释，尽管考虑到变量的顺序应该是一致的，只有一种方法可以将图形合并在一起，并且维护这种顺序的规则可能很简单足够了（我还没有将它们正式化，但我对这些是什么有了一个大致的了解）。

Answer 1

对于“合并”，Minato 的意思是 union (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 卷第 7.1.4 节中有详细解释（问题 199 的答案是相关的）。所有这些的总体思路是，他们认为两个子图，代表所有的集合与变量v和所有的设置不变量v分别（这两者都是平凡中发现，如果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