Objectives:

• Use the Shannon expansion to create Reduced Ordered Binary Decision Diagrams (ROBDDs) from arbitrary Boolean formulas
• See how variable ordering affects the size of a resulting ROBDD
• Use the if-then-else (ITE) algorithm to implement Boolean operations
• Create new ROBDDs that represent new Boolean functions using ITE

## Problems

1. (10 points) Use the Shannon expansion to create an ROBDD for the predicate $F(a,b,c,d) = (a \wedge b) \vee (\neg a \wedge c) \vee (b \wedge \neg c \wedge d)$ with the following variable order $a < b < c < d$. Show the complete tree from the Shannon expansion, the complete unique table, and the graphical depiction of the final ROBDD.

2. (10 points) Repeat problem 1 only this time use the variable order $d < c < b < a$.

3. (10 points) Suppose you have ROBDDS, $f$ and $g$. What is the ITE call or calls to compute the following functions?

• $f \wedge g$
• $f \vee g$
• $\neg f$
• $\neg(f \wedge g)$
• $f \rightarrow g$
• $f \leftrightarrow g$

4. (20 points) Repeat problem 1, only this time, rather than use the Shannon expansion directly, use the ITE algorithm. Initialize the unique table with ROBDD nodes for variables $a$, $b$, $c$, and $d$. Show each call to ITE.

5. (20 points) Repeat problem 4, only this time us the variable order $d < c < b < a$.

6. (20 points) Suppose you have two additional variables $e$ and $f$ such at $a < b < c < d < e < f$. Apply the replace algorithm on the BDD from problem 4 such that $c$ is replaced with $f$ and $d$ is replaced with $e$. This method is BDD::SwapVariables in the Cudd package. Show the added entries to the unique table, the calls to ITE, and draw the final BDD.

7. (20 points) Install CUDD 3.0.0 and use it to compare to the BDDs in problems 4, 5, and 6. Submit the graphs for each BDD using DumpDot with the code to generate them. See cudd/cudd-example.cc for an example on how to use CUDD 3.0.0. Graphviz is also required for this problem to create the PDF files of the BDDs.