= Solution
A <reduced ordered binary decision diagram> is obtained by sharing equal <terminal nodes>, removing a <decision node> whose two children are equal, and sharing <decision nodes> with the same tested <Boolean variable> and the same ordered pair of children. Apply these rules to the <binary decision tree> in part (c) as follows.
* Merge the three zero <terminal nodes> into one zero <terminal node>, and merge the five one <terminal nodes> into one one <terminal node>.
* At $(z,y)=(0,0)$ the $x$ <decision node> has children $(0,0)$. Remove it and redirect its incoming arrow to zero.
* At $(z,y)=(0,1)$ and $(z,y)=(1,1)$ the two $x$ <decision nodes> each have children $(1,1)$. Remove both and redirect their incoming arrows to one.
* The remaining $x$ <decision node>, at $(z,y)=(1,0)$, has children $(0,1)$, so retain it.
* The $y$ <decision node> under $z=0$ now has children $(0,1)$, while the one under $z=1$ has children $(x,1)$. These are different, so neither can be merged or removed. The top $z$ <decision node> also has different children.
The left panel below is therefore the resulting <reduced ordered binary decision diagram>. Its full description is
|| <Decision node>
|| Test
|| Zero child
|| One child
| $r$
| $z$
| $u$
| $v$
| $u$
| $y$
| 0
| 1
| $v$
| $y$
| $w$
| 1
| $w$
| $x$
| 0
| 1
There are $\boxed{4+2=6}$ <vertices>: four <decision nodes> and two <terminal nodes>.
\Image[/past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/formal-verification-2015-decision-diagrams.png]
{title=Reduced ordered decision diagrams: reversing the given order preserves its size, while testing y first saves one decision node}
The original <binary decision diagram> also has four <decision nodes> and two <terminal nodes>, and is already reduced for $x<y<z$: the two $y$ <decision nodes> have different children and no <decision node> has two equal children. Thus \b[reversing the order has not made this example smaller]. Indeed $y\lor(x\land z)$ is unchanged by interchanging $x$ and $z$, and the new <binary decision diagram> is the original one with those two labels exchanged. The uniqueness of a <reduced ordered binary decision diagram> applies to a fixed <variable ordering of a binary decision diagram>; it does not assert that every ordering has the same size.
Back to article page
