Binary decision diagram

A Binary Decision Diagram (BED; engl binary decision diagram, BDD. ) Is a data structure for representing Boolean functions. Binary decision diagrams are used primarily in the area of ​​hardware synthesis and verification.

Definition

A binary decision diagram is an acyclic, directed graph with a root, so is true that

  • Each node is either a leaf or an internal node.
  • Leaves have no outgoing edges and are labeled with a value from.
  • Each internal node has exactly two outgoing edges, which are referred to as low - or high edge. The endpoints of these edges are denoted by or. In addition, each internal node is labeled with a variable.
  • On all paths from the root to a leaf are the variables in a firm, strict order sorted ( variable ordering, OBDD ).
  • All isomorphic subgraphs are merged and there is no node whose children are the same ( reduction ROBDD ).

By Shannon decomposition that shown by a binary decision diagram Boolean function can be computed. Be from a node of the binary decision diagram. The function is defined as shown by

  • If a sheet, then the function is the value represented by the label
  • If an internal node with label is, then.

Exists for every Boolean function ( with fixed variable order ) exactly one minimal OBDD, ie OBDDs are a canonical representation of Boolean functions ( Bryant, 1986).

Example

This image provides a free, orderly and reduced binary decision diagram dar. The low - edge of a node is represented by solid lines and dashed the high edge. The variable order used is. The displayed function can be calculated as follows:

  • Nodes:
  • Left node:
  • Right - node:
  • Nodes:

We can also evaluate the function shown directly for a given variable assignment. For this, only the path associated with the assignment will be followed until they reached a leaf. The value of this paper is the function value for the given variable assignment.

Suppose we want to determine for the above example the function value. We start at the root of the binary decision diagram. This node is labeled with. Since in our assignment, we follow the low - edge and reach a node that is labeled with. It is true, so we follow the high - edge and reach the leaf labeled 0 Consequently applies.

Variable orders

The structure and the number of nodes of a parent and reduced binary decision diagram depend on many features strongly on the chosen variable ordering. As an example, consider the Boolean function. If you choose for the variable order, the binary decision diagram requires more than knots. In the variable order, however, fulfill nodes.

There are also functions that require exponentially many nodes regardless of the variable ordering in the number of variables. This includes such important features as the multiplication. Therefore, over the years, many variants of binary decision diagrams have been developed, such as Kronecker Functional Decision Diagrams, Binary Moment Diagrams, Edge -valued binary decision diagrams and numerous others.

Operations on binary decision diagrams

The operations that are normally provided by all implementations available, at least the Boolean operators conjunction ( AND), disjunction are (OR ), and negation (NOT).

The negation can be carried out by the 0 - reversed and the 1- leaf of the binary decision diagram. The remaining two -digit Boolean operations are normally limited to one special ternary operator, called the ITE - operator returned:

The name comes from ITE if-then -else: If the argument is 1, then the function value of ITE is equal to the function value, otherwise equal to that of.

With the help of ITE, we can write:

One can easily convince them that allows all 16 binary Boolean operations expressed using the ITE operator. Consequently, it is sufficient to provide an implementation of the ITE operator.

Another important operations are, for example:

  • Test of two functions shown for equality. Most of the available implementations ensure that nodes that represent the same function will be applied only once. Then just may be compared to the nodes of the binary decision diagram pointers: they are the same, so the functions and vice versa shown. So that the constant term (i.e., ).
  • Test for satisfiability of the function shown, so to answer the question of whether there is an assignment to the variables, so that the function takes the value 1. To this end, the binary decision diagram only has to be compared with the 0 - sheet.
  • Calculating the number of satisfying assignments: can be done in linear time decision diagram by traversing the binary. See details.

Implementations

  • CMU BDD, BDD package, Carnegie Mellon University, Pittsburgh
  • CUDD: BDD package, University of Colorado, Boulder
  • CrocoPat: BDD package with interpreter for Relational Programming, University of California, Berkeley
  • JINC: A parallel ( multi-threading ) C Library, University of Bonn.
Randal Bryant Run time (program lifecycle phase) Ingo Wegener Donald Knuth
125665
de