Module biodivine_lib_bdd::tutorial::p01_bdd_intro

Introduction to BDDs

BDD is a directed acyclic graph (DAG) with two types of vertices (or nodes). There are two terminal vertices called 1 and 0 which have no outgoing edges. The rest of the vertices are decision vertices. Each decision vertex has an associated Boolean variable $v$ and two outgoing edges $low$ and $high$. In diagrams, $low$ edges are typically drawn as dashed and $high$ edges as solid. The graph has always one root vertex (with no predecessors).

Semantically, for a given valuation (assignment) of Boolean variables $Var \to \{ 0, 1 \}$, we can “evaluate” the graph by starting in the root vertex and choosing the following vertex based on the value of the current decision variable in the given valuation. Once we reach a terminal vertex, we obtain a final Boolean value. For example, consider the formula $a \land \neg b$. The corresponding BDD is the following:

graph LR
    a($a$)
    b($b$)
    zero($0$)
    one($1$)
    a -.-> zero
    a --> b
    b -.-> one
    b --> zero

We can see that there is only one path from the root ($a$) to 1 and this path corresponds to the only valuation which satisfies the Boolean formula (i.e. $a = 1; b = 0$).

Typically, BDDs assume some fixed ordering of variables such that every path from root to terminal follows this ordering (thus ordered). Furthermore, in every BDD, all redundant vertices are removed (thus reduced). The vertex is redundant if both $low$ and $high$ point to the same vertex (there is no decision) or if there is another vertex with the same values of $v$, $low$ and $high$ somewhere else in the graph (we can reuse this vertex).

When the BDD is ordered and reduced, it is canonical, i.e. every equivalent Boolean formula has the same BDD (equality can be thus checked syntactically on the structure of the graph).

Encoding BDD in an array

While BDD is a graph, it would be wasteful to store each node of the BDD as a separate memory object requiring allocations and book keeping. Instead, we sort nodes in each BDD in the DFS post-order (taking low edge first and high edge second, although this decision is arbitrary) of the graph and this way, we can easily save them as a sequence in an array. The only exception are the two terminal nodes which we always place on positions 0 and 1 (empty BDD only has the 0 node).

Because DFS post-order is unique, we can still check formula equivalence by comparing the two arrays element-wise. Also notice that the root of the BDD is always the last element of the array and children of any node always have smaller indices than the parent.

The BDD from the previous section translates to the following array:

[0, 1, (b, low = 1, high = 0), (a, low = 0, high = 2)]

Notice that the edge pointers are now indices into the array itself instead of memory references. This also allows certain memory optimisations (for “small” BDDs, the pointers only need to be 32 bits even on 64 bit platforms, etc.). Also, such representation is trivial to serialize, deserialize or share, since we can just clone the whole array if needed.