Solution

ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/computer-aided-formal-verification/1/c/solution

For a complete binary decision tree with variable ordering of a binary decision diagram , first test , then , then 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 . The repeated tests are intentional: this is the full binary decision tree before any reduction.
Figure 1.
Complete decision tree for the ordering z, y, x; dashed edges test zero and solid edges test one
. Details.
For example, the branch ends at one, whereas ends at zero. This checks the dependence on that must survive the later reduction.

New to topics? Read the docs here!