Next: Pattern Matching: CNF Up: Reference - Preprocessing Previous: Reference - Preprocessing   Contents

Binary Decision Diagrams (BDDs)

A Binary Decision Diagram (BDD) is a rooted, directed acyclic graph. A BDD is used to compactly represent the truth table, and therefore complete functional description, of a Boolean function. Vertices of a BDD are called terminal if they have no outgoing edges and are called non-terminal otherwise. There is one non-terminal vertex, called the root, which has no incoming edge. There is at least one and there are at most two terminal vertices, one labeled 0 and one labeled 1. Non-terminal vertices are labeled to represent the variables of the corresponding Boolean function. A non-terminal has exactly two outgoing edges, labeled T and/or F, and the vertices incident to edges outgoing from vertex v are called and , respectively. Associated with any non-terminal vertex v is an attribute called which satisfies the properties and if and only if vertices v and w have the same labeling (that is, correspond to the same variable). Thus, the index attribute imposes a linear ordering on the variables of the BDD.

A Reduced Ordered Binary Decision Diagram (ROBDD) is a BDD such that: 1) There is no vertex v such that ; 2) The subgraphs of two distinct vertices v and w are not isomorphic. A ROBDD represents a Boolean function uniquely in the following way. Define , v a vertex of the ROBDD, recursively as follows:

1. If v is the terminal vertex labeled F, then ;
2. If v is the terminal vertex labeled T, then ;
3. Otherwise, if v is labeled x, then .
Then is the function represented by the ROBDD. Observe that a Boolean function has different ROBDD representations, depending on the variable order imposed by index, but there is only one ROBDD for each ordering. Thus, ROBDDs are known as a canonical representation of Boolean functions. Observe also that a path from root to terminal in a ROBDD corresponds to one or more rows of a truth table associated with the function represented by the ROBDD: the labels of the vertices encountered on the path are the variables and their assigned values are determined from the outgoing edges traversed, the assignment being T (F) if the true (false) edge is taken, respectively. The collection of all paths specifies the truth table completely. Although ROBDDs are actually used internally in SBSAT, they are referred to as BDDs in this manual.

Figure  shows an example of a BDD and the function it represents. See the data structures section for details on how the BDDs are implemented in SBSAT. The following are some simple BDD operations that are used by preprocessing operations which are described in subsequent sections.

A BDD is constructed by attaching BDDs and , representing a true and a false branch, respectively, to a vertex v with some labeling x representing the root. We may think of the operation to do this as being the following, in pseudo C++ style:

BDD ite(variable x, BDD , BDD );

That is, ite returns a BDD with root v labeled x and such that and . But the actual construction is such as to avoid building BDDs which are isomorphic to existing ones, so the following is used to implement the construction instead (it is too complicated to state here):

BDD find_or_add_node (variable x, BDD , BDD );

This operation returns an existing BDD if there is one that matches ite(x, , ) already, and otherwise builds a new BDD with root v labeled x, true branch and false branch (that is, false(v) = and true(v) = ). The BDDs and/or may have to be constructed as well.

The following two simple operations are used several times in describing important BDD operations in subsequent sections. They are given in pseudo C++ style:

BDD Reduce (variable x, BDD f) {
if (root(f) == x) return true(root(f));
return f;
}

BDD Reduce (variable x, BDD f) {
if (root(f) == x) return false(root(f));
return f;
}

Reduce(,) returns constrained by the assignment of T to variable and Reduce(,) returns constrained by the assignment of F to the variable .

Next: Pattern Matching: CNF Up: Reference - Preprocessing Previous: Reference - Preprocessing   Contents
John Franco 2011-09-15