= Solution
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
|| $z$
|| $y$
|| $f$
| 0
| 0
| 0
| 0
| 1
| 1
| 1
| 0
| $x$
| 1
| 1
| 1
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.
\Image[/past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/formal-verification-2015-decision-tree.png]
{title=Complete decision tree for the ordering z, y, x; dashed edges test zero and solid edges test one}
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.
Back to article page
