Binary decision diagrams
Design an abstract datatype for binary decision diagrams (BDDs).
A BDD is a representation of a Boolean function of several variables.
It can be defined recursively as 0 (false) or 1 (true) or a
decision structure of the form "if v then f1 else f0"
where f1 and f0 are themselves BDDs, with some additional constraints:
- the order in which variables are tested from root to leaves in f1 and f0 is the same
- there are no needless tests, i.e. "if v then f else f" is represented as f.
- any common sub-diagrams are shared (see the last example here)
Define a data structure to represent a BDD. For simplification, choose a simple
set of variable names: characters ('a', 'b', 'p', 'q', etc.) or numbered variables: v0, v1, v2, ...
Your abstract datatype should have
- constants or functions bdd_one and bdd_zero for the BDDs 1 (true) and 0 (false)
- a function bdd_ite (if-then-else) that constructs the BDD for "if vk then f1 else f0" where f1 and f0 are BDDs and all their variables are after vk in the variable ordering.
To respect the constraint that all common sub-diagrams should be shared, keep a hashtable of all constructed BDDs (hash by a combination of variable, left pointer and right pointer). Whenever you need to construct an if-then-else node, first check if it exists in the hash table and return it; only otherwise construct a new node.
- a function bdd_print that prints a BDD in a way that can easily be displayed, for instance in the DOT format, like this example for (v1 OR v2) AND v3. If you have the graphviz package installed, you can view such a file with the command dotty bdd.dot or generate a PDF: dot -Tpdf bdd.dot -o bdd.pdf. You can also visualize it online.
(A directed graph is given by nodes and edges with optional labels and attributes. The given example labels intermediate nodes with integers derived from pointer values. Optionally, try to print a shared node only once, e.g. the node labeled v3 in the given example.)
- functions that compute AND and OR for two BDDs. Construct the result recursively: given f = if v then f1 else f0 and g = if v then g1 else g0, we have f AND g = if v then f1 AND g1 else f0 AND g0.
Marius Minea
Last modified: Fri Mar 18 21:00:00 EET 2016