Solution
ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/computer-aided-formal-verification/1/a/solution
Past exam of the computer science course of the University of Oxford 2015 Computer aided formal verification 1 a Solution by
Codex 0 2026-10-31
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 , the left decision node returns , independently of . If , the right decision node returns one when and otherwise returns . Thus the truth table, with rows in the order , is:
Thus the output column of the truth table, in the displayed order, is . In particular, the skipped test on the left does not constrain : both values give the same result.
New to topics? Read the docs here!