Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Intersection of Zero-Suppressed BDD -- Implementing polynomials using ZDDs

I'm trying to implement univariate polynomials using ZDDs, as suggested in a comment in an other question.

I've read the paper of S. Minato(you may download it here), but I don't understand how to implement the operations on these ZDDs.

The idea in the paper is that polynomials can be represented using x^(2^i) as variables. For example x^5 + x^3 + x can be rewritten as x^4x^1 + x^2x^1 + x^1, if you create nodes for each x^(2^i) variable and connect with the "1-edge" variables that are multiplied together and with the "0-edge" variables that are added together you can easily obtain a graph representing that polynomial. The ZDDs are graphs of this kind that enforce some condition on the graph(for more information read the article of Minato and the wikipedia's page on BDDs)

The coefficients can be similarly represented using sums of powers of 2 (e.g. 5 = 2^2 + 2^0 etc. With every 2^i being a variable and the nodes are connected with 1- and 0-edges in the same fashion).

Now, my problem is the algorithm for addition of two ZDDs. The algorithm seems quite simple:

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.

The problem is: how can I find "C" and "S" efficiently?

The author provides code for the multiplication, but the code is actually trivial once you have the previous algorithms implemented. And since these algorithms are not provided also the multiplication one is "useless".

Also the notion of "merge" ZDDs is not well explained, even though, considering the fact that the order of the variables should be consistent, there is only one way to merge the graphs together, and the rules to maintain this order are probably simple enough(I did not formalize them yet, but I've got a rough idea of what these are).

like image 753
Bakuriu Avatar asked Sep 30 '12 18:09

Bakuriu


1 Answers

With "merge" there Minato means union (algorithm). You can see this from the example, too:

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

The idea is that the inner sets represent products and the whole ZDD represents the sum of those products, so if you just OR (aka union or merge) in some more sets, they're effectively added.

The complete summation algorithm actually just does (A xor B) + 2 * (A and B) (recursively) which is equivalent to the familiar bitwise addition algorithm, but the xor was written as (A or B) without (A and B).

That also makes it obvious why simply taking the union is OK when there are no common combinations - if A and B is empty, A xor B is the same as A or B and the "carry" is zero.

The algorithms for OR, AND, XOR and BUTNOT are explained in detail in The Art of Computer Programming volume 4, section 7.1.4 (the answer to question 199 is relevant). The general idea for all of them is that they consider the two sub-graphs that represent all the sets with the variable v and all the sets without the variable v separately (which are both trivially found if v is the topmost variable in one or both arguments as either the low and high children or the input itself), and then combining the result.

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
like image 138
harold Avatar answered Oct 21 '22 11:10

harold