Past exam of the computer science course of the University of Oxford / 2015 / Computer aided formal verification / 1

Follow the binary decision diagram from its top decision node to a terminal node, choosing the outgoing arrow specified by each tested Boolean variable. If $x=0$, the left $y$ decision node returns $y$, independently of $z$. If $x=1$, the right $y$ decision node returns one when $y=1$ and otherwise returns $z$. Thus the truth table, with rows in the order $(x,y,z)$, is:

Thus the output column of the truth table, in the displayed order, is $\boxed{(0,0,1,1,0,1,1,1)}$. In particular, the skipped $z$ test on the left does not constrain $z$: both values give the same result.

Splitting the Boolean function according to the first tested Boolean variable givesThe identity $y\vee (\neg y\wedge z)=y\vee z$ follows by considering $y=0$ and $y=1$. Using it and distributing Boolean conjunction over Boolean disjunction,The first two terms combine to $y$ because $x\vee \neg x=1$. This also explains the truth table: $y=1$ always makes the output one, while with $y=0$ the output is one exactly when both $x$ and $z$ are one.

For a complete binary decision tree with variable ordering of a binary decision diagram $z<y<x$, first test $z$, then $y$, then $x$ on every branch. The four Boolean cofactors after the first two tests are

The eight terminal nodes, read from left to right in the figure, are $\boxed{0,0,1,1,0,1,1,1}$. The repeated tests are intentional: this is the full binary decision tree before any reduction.

For example, the branch $z=1,y=0,x=1$ ends at one, whereas $z=0,y=0,x=1$ ends at zero. This checks the dependence on $z$ that must survive the later reduction.

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.

The left panel below is therefore the resulting reduced ordered binary decision diagram. Its full description is

There are $\boxed{4+2=6}$ vertices: four decision nodes and two terminal nodes.

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 reversing the order has not made this example smaller. Indeed $y\vee (x\wedge 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.

Choose the variable ordering of a binary decision diagram $y<x<z$. The Boolean cofactor with $y=1$ is the constant one, while the Boolean cofactor with $y=0$ is $x\wedge z$. Consequently the right panel in part (d) has the following arrows:Here an entry such as $0\to x$ denotes the zero arrow to the $x$ decision node. There are $\boxed{3+2=5}$ vertices: three decision nodes and two terminal nodes, saving one decision node relative to either of the previous orderings. Testing $y$ first is effective because its one branch settles the entire Boolean function immediately. The ordering $y<z<x$ works equally well.

This is also minimal among ordinary binary decision diagrams for this Boolean function. Each Boolean variable is essential: setting $y=0,z=1$ leaves $f=x$; setting $y=0,x=1$ leaves $f=z$; and setting $x=z=0$ leaves $f=y$. If a Boolean variable were never tested, the represented Boolean function could not depend on it. Thus at least three decision nodes are necessary, and the construction attains that bound.

A transition relation requires an explicit interpretation of the Boolean variables as current and next state bits. Take the four states $q_{00},q_{01},q_{10},q_{11}$. Encode the current state by $(u,x)$ and the next state by $(y,z)$, and defineThe extra current bit $u$ is deliberately unused by the Boolean formula. A four-state transition system normally needs four bits to describe a pair of states; a Boolean formula using only three of them simply describes a transition relation independent of the fourth bit.

When $x=0$, the condition is $y=1$, so the permitted next states are $q_{10}$ and $q_{11}$. When $x=1$, the condition is $y\vee z$, so the permitted next states are $q_{01},q_{10},q_{11}$. The resulting adjacency matrix, with rows and columns both ordered $q_{00},q_{01},q_{10},q_{11}$, isThe directed graph below plots all ten directed edges, including the three self-loops. No arrow enters $q_{00}$, but it is a valid state with two outgoing arrows. Every state has a successor. As permitted, no initial states are distinguished.