implementation - 零抑制 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-边”变量以及相加的“0-边”变量连接，您可以轻松获得表示该多项式的图形。 ZDD 是这种在图上强制执行某些条件的图(有关更多信息，请阅读 Minato 的文章和维基百科关于 BDD 的 page)

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

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

If F and G (ZDDs)have no common combinations, the addition (F + G) can be completed by just merging them. When they contain some common combinations, we compute the following formulas: (F + G) = S + (Cx2), where C = F ∩ G, S = (F U G) \ C . By repeating this process, common combinations are eventually exhausted and the procedure is completed.

问题是:如何有效地找到“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 的答案是相关的)。他们所有的一般想法是，他们考虑代表所有带有变量 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