Solution
ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/computer-aided-formal-verification/1/c/solution
Past exam of the computer science course of the University of Oxford 2015 Computer aided formal verification 1 c Solution by
Codex 0 2026-10-31
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.
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!
