Polynomial representations as ZDD
This site will visually introduce polynomial representations as ZDD. A Boolean polynomial is a (multivariate) polynomial over the finite field with two elements, where every exponent is at most one per variable Using ZDDs we describe a term structure of a Boolean polynomial. A term occurs in it, if a valid path (ending at one) corresponds to it: a variable occurring in the polynomial, if and only if the path follows a then branch in the graph.We start with a variable x:
Multiplication
Example: x
![x x](img/formulas/x.png)
Example: x*y
![x*y x*y](img/formulas/x_times_y.png)
Example: x*y*z
![x*y*z x*y*z](img/formulas/x_times_y_times_z.png)
![0-th image](img/formulas/x_times_y_times_z_term_0.png)
Addition
After getting a picture, how multiplication of variables look like, we have a look at addition:
We the polynomial x+y
Example: x+y
As we can see, there are now two path leading two the terminal 1-node.
![0-th image](img/formulas/x_plus_y_term_0.png)
![1-th image](img/formulas/x_plus_y_term_1.png)
Example: x+y+z
![x+y+z x+y+z](img/formulas/x_plus_y_plus_z.png)
![0-th image](img/formulas/x_plus_y_plus_z_term_0.png)
![1-th image](img/formulas/x_plus_y_plus_z_term_1.png)
![2-th image](img/formulas/x_plus_y_plus_z_term_2.png)
More polynomials
After getting a fundamental understanding for these, very simple polynomials, we try to understand more complicated examples. We add 1 to the polynomial the above presented polynomial x*y*z and get the following picture for x*y*z+1:Example: x*y*z+1
![x*y*z+1 x*y*z+1](img/formulas/x_times_y_times_z_plus_one.png)
![0-th image](img/formulas/x_times_y_times_z_plus_one_term_0.png)
![1-th image](img/formulas/x_times_y_times_z_plus_one_term_1.png)
Example: x*y*z+x
![x*y*z+x x*y*z+x](img/formulas/x_times_y_times_z_plus_x.png)
![0-th image](img/formulas/x_times_y_times_z_plus_x_term_0.png)
![1-th image](img/formulas/x_times_y_times_z_plus_x_term_1.png)
Example: x*y*z+y
![x*y*z+y x*y*z+y](img/formulas/x_times_y_times_z_plus_y.png)
![0-th image](img/formulas/x_times_y_times_z_plus_y_term_0.png)
![1-th image](img/formulas/x_times_y_times_z_plus_y_term_1.png)
Example: x*y*z+z
![x*y*z+z x*y*z+z](img/formulas/x_times_y_times_z_plus_z.png)
![0-th image](img/formulas/x_times_y_times_z_plus_z_term_0.png)
![1-th image](img/formulas/x_times_y_times_z_plus_z_term_1.png)
Special sets
In this section, I will represent a few very structured polynomials with a structured diagram. First of all, I represent the polynomial (a+1)*(b+1)*(c+1)*(d+1)*(e+1) containing every monomial in the variables a, b, c, d, e. The polynomials has 32 terms, but the graph contains only 5 non-terminal nodes and 10 edges. Starting from the root node, on each of the five levels, we can choose the then or else branch and will always end at the terminal 1-node (so get a valid path). Combinatorial this means, that we have five times a choices of two possibilities, so we get 32 combinations, which is exactly the number of terms.Example: (a+1)*(b+1)*(c+1)*(d+1)*(e+1)
![(a+1)*(b+1)*(c+1)*(d+1)*(e+1) (a+1)*(b+1)*(c+1)*(d+1)*(e+1)](img/formulas/allmonomials.png)
Example: a*(b+c+d+e)+b*(c+d+e)+c*(d+e)+d*e+a+b+c+d+e+1
![a*(b+c+d+e)+b*(c+d+e)+c*(d+e)+d*e+a+b+c+d+e+1 a*(b+c+d+e)+b*(c+d+e)+c*(d+e)+d*e+a+b+c+d+e+1](img/formulas/maxdeg2.png)
Example: a*(b+c+d+e)+b*(c+d+e)+c*(d+e)+d*e
![a*(b+c+d+e)+b*(c+d+e)+c*(d+e)+d*e a*(b+c+d+e)+b*(c+d+e)+c*(d+e)+d*e](img/formulas/deg2.png)
Lexicographical ordering/Natural path ordering
In all these examples, the rightmost path consists only of then branches and leads to the terminal 1-node. While the first is of course a consequence of, that we try to let then branches go to the right, the second might be in the first moment surprising, but is very general and reflects the fact, that ZDDs are reduced (letting out redundant nodes): If the then branch of a node leads to zero, this means that only the else branch (terms in which the variable corresponding to the node doesn't occur) contributes the the term structure of that (sub-) polynomial, so the node doesn't give more information on our term structure and we can leave it out. Note, that other forms of diagrams like ROBDDs can have other rules for the implicit elimination of nodes and its meaning. In this way, always choosing the then path determines a naturally biggest path. This corresponds to searching a term with early variables have an as exponent as high as possible (one), which is the lexicographically leading term of a polynomial. In a similar way we can define a natural order on the valid paths of the graph, which corresponds just to the lexicographical ordering of terms in a Boolean polynomial. The following sequence of images illustrates the natural path ordering. Each picture highlights an path (ordered by the natural ordering, which corresponds to the lexicographical monomial ordering).
![0-th image](img/formulas/highlight_term_lp_0.png)
![1-th image](img/formulas/highlight_term_lp_1.png)
![2-th image](img/formulas/highlight_term_lp_2.png)
![3-th image](img/formulas/highlight_term_lp_3.png)
![4-th image](img/formulas/highlight_term_lp_4.png)
![5-th image](img/formulas/highlight_term_lp_5.png)
![6-th image](img/formulas/highlight_term_lp_6.png)
![7-th image](img/formulas/highlight_term_lp_7.png)
We provide a second less structured example, which shows the natural ordering of path: the polynomial a*b + a*c*d + a + b*c*d*e + b*c*e + b
![0-th image](img/formulas/second_highlight_term_lp_0.png)
![1-th image](img/formulas/second_highlight_term_lp_1.png)
![2-th image](img/formulas/second_highlight_term_lp_2.png)
![3-th image](img/formulas/second_highlight_term_lp_3.png)
![4-th image](img/formulas/second_highlight_term_lp_4.png)
![5-th image](img/formulas/second_highlight_term_lp_5.png)
This explains, why the lexicographical ordering works very natural for polynomials in ZDD representation. However, we have implemented quite sophisticated implementations of important other orderings (leading term calculation and ordered iteration) in PolyBoRi:
- Degree lexicographical ordering
- (Ascending) Degree reverse lexigraphical ordering
- Block orderings (for degree ordered blocks)
To contrast the natural path ordering, we display the paths of the same polynomial now in degree lexicographical ordering.
![0-th image](img/formulas/highlight_term_dlex_0.png)
![1-th image](img/formulas/highlight_term_dlex_1.png)
![2-th image](img/formulas/highlight_term_dlex_2.png)
![3-th image](img/formulas/highlight_term_dlex_3.png)
![4-th image](img/formulas/highlight_term_dlex_4.png)
![5-th image](img/formulas/highlight_term_dlex_5.png)
![6-th image](img/formulas/highlight_term_dlex_6.png)
![7-th image](img/formulas/highlight_term_dlex_7.png)
Also for the second example (a*b + a*c*d + a + b*c*d*e + b*c*e + b), we show the ordering of paths corresponding to degree lexicographical ordering
![0-th image](img/formulas/second_highlight_term_dlex_0.png)
![1-th image](img/formulas/second_highlight_term_dlex_1.png)
![2-th image](img/formulas/second_highlight_term_dlex_2.png)
![3-th image](img/formulas/second_highlight_term_dlex_3.png)
![4-th image](img/formulas/second_highlight_term_dlex_4.png)
![5-th image](img/formulas/second_highlight_term_dlex_5.png)
The iterators implemented in PolyBoRi calculate successively the valid paths of a ZDD (terms of the polynomial). This calculation of the next path depends essentially just on the current path. Moreover they use only the ZDD structure of the polynomial, to avoid conversions. This is very important for performance, if you iterate just over the first few terms.
Dependence of ZDDs on the order of variables
It is quite obvious, that the form of the ZDDs depends on the ordering of variables: In the trivial cases, just some nodes are switch. However, usually the ZDD can look very different.
We start with an easy example: The polynomial a*b+a*c+a+1
Example: a*b+a*c+a+1
![a*b+a*c+a+1 a*b+a*c+a+1](img/formulas/a_times_b_plus_a_times_c_plus_a_plus_1_forward.png)
If we reverse the ordering of variables, the image just looks as follows:
Example: a*b+a*c+a+1, reversed order
![a*b+a*c+a+1, reversed order a*b+a*c+a+1, reversed order](img/formulas/a_times_b_plus_a_times_c_plus_a_plus_1_backward.png)
Example: a*b+a*c+a+1
![a*b+a*c+a+1 a*b+a*c+a+1](img/formulas/a_times_b_times_c_plus_a_times_b_plus_a_times_c_plus_1_forward.png)
Again, the reversing the ordering of variables, changes the form of the ZDD:
Example: a*b+a*c+a+1, reversed order
![a*b+a*c+a+1, reversed order a*b+a*c+a+1, reversed order](img/formulas/a_times_b_times_c_plus_a_times_b_plus_a_times_c_plus_1_backward.png)
While the differences above were in an expectable magnitude and the polynomials looked quite artificial, we continue with the highest carry BIT of an 3-bit adder. First we start we the naive alphabetical ordering of variables:
Example: Carry BIT 3-bit adder
![Carry BIT 3-bit adder Carry BIT 3-bit adder](img/formulas/carry_bit3_alphabetical.png)
The ZDD looks quite huge and not very structured. But if we optimize the ordering of variables, the graph looks like that:
Example: Carry BIT 3-bit adder, topological ordered
![Carry BIT 3-bit adder, topological ordered Carry BIT 3-bit adder, topological ordered](img/formulas/carry_bit3_optimized.png)
Using this ordering of variables makes also the polynomial computations much faster.