Solution

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

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!