# Reordering Binary Decision Diagrams

This tool can be used to compute BDDs for a set of given formulas and a given variable ordering. The tool will print the BDDs for all of these formulas together and therefore also shows how common subtrees are shared. Zero leafs are omitted unless you change the style. The tool then computes a swap sequence to change the first given variable ordering to the second one and will print the BDDs for the intermediate variable orderings step by step. Finally, Sifting is applied to improve the second variable ordering.

 style show false leaf suppress false leaf variable order 1: variable order 2: formulas x0 ⊕ y0 ⊕ c0; x1 ⊕ y1 ⊕ ( c0 ∧ (x0 ∨ y0) ∨ (x0 ∧ y0))); x2 ⊕ y2 ⊕ ( (c0 ∧ (x0 ∨ y0) ∨ (x0 ∧ y0)) ∧ (x1 ∨ y1) ∨ (x1 ∧ y1))); x3 ⊕ y3 ⊕ (((c0 ∧ (x0 ∨ y0) ∨ (x0 ∧ y0)) ∧ (x1 ∨ y1) ∨ (x1 ∧ y1))) ∧ (x2 ∨ y2) ∨ (x2 ∧ y2)))

Some remarks on the default values chosen: The 4-bit sum (s3,s2,s1,s0) of two 4-bit numbers (x3,x2,x1,x0) and (y3,y2,y1,y0) with an initial carry c0 can be computed with the above propositional formulas. The first ordering chosen is the best variable ordering for all functions together. Have a look at these BDDs and find the BDDs for the function si and also find the BDDs for the carry bits ci used to determine si as xi ^ yi ^ ci as well as the BDDs of their negations !ci. Then, you will see that the size of the BDD for n-bit addition is exactly 9n-4, so addition can be represented by linear sized BDDs. The second variable ordering will then lead to an exponential size of the BDDs, so that addition can also become exponential when using bad orderings. Sifting will finally reduce that even though it does not find the optimal ordering.