Difficulty: **
This was one of our first attempts to produce an extended three-hour test with the now traditional ‘sting in the tail’. The original version started out with an interpreter for boolean expressions, which then led to functions for implementing negation and satisfiability on BDDs. The last two parts were concerned with the construction of BDDs and ROBDDs. The average mark was around 72%, with most students reaching Part III at least within the three hours. Quite a few students completed all four parts; the sticking point for many was the ‘inverse lookup’ required for the ROBDD construction.
In hindsight, I have come to the conclusion that negation of BDDs was uninteresting, as it involves nothing more than flipping the $False$ and $True$ terminal nodes. I also think that it is more useful to learn about the notion of restriction of boolean expressions, as it facilitates the Shannon expansion:
$E \equiv x \rightarrow E [True/x], \,E[False/x]$
Restriction also leads to a more efficient algorithm for constructing BDDs.
The version you see here is thus a slightly re-worked version of the original test, with boolean expression evaluation being replaced by restriction. The last two parts are unaltered versions of the original, bar the use of restriction to construct the (RO)BDDs.
If you want something else to practice on, try writing the original eval function, which has type
eval :: BExp -> Env -> Bool and rewrite the two make functions in terms of eval.
Specification
Template File
More Information
An excellent introduction to BDDs and their construction and use can be found in Henrik Anderson’s lecture notes: An Introduction to Binary Decision Diagrams. An alternative Haskell implementation of ROBDDs can be found here.