Binary decision diagram

from Wikipedia, the free encyclopedia

A binary decision diagram ( BED ;. Engl decision binary diagram , BDD ) is a data structure to represent Boolean functions . Binary decision diagrams are mainly used in the field of hardware synthesis and verification .

A BED can be understood as a kind of flow diagram for evaluating a Boolean function . Here, one after the value of variable , interrogated ..., with the two choices True or False , which branch each in different parts of the diagram. The result is the value of the Boolean function under the selected variable assignment . The presentation of the diagram is largely compressed, so that questions irrelevant to the result are left out and duplicate partial diagrams are merged.

definition

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

  • Each knot from is either a leaf or an inner knot.
  • Sheets have no outgoing edges and are labeled with a value of .
  • Each inner node has exactly two outgoing edges, which are referred to as low and high edges. The end points of these edges are denoted by or . In addition, each inner node is labeled with a variable .

Such a BED is called ordered (variable order, OBDD) if the variables appear in the same order on all paths starting from the root.

A BED is called reduced (RBDD) if the following two operations have been applied exhaustively:

  • Every two isomorphic subgraphs are merged into one
  • Elimination ("bridging") of nodes whose two endpoints are identical

The term binary decision-making diagram generally includes the requirements for variable ordering and reduction. The advantage of these properties is that there is exactly one reduced, ordered BED for each Boolean function (with a fixed variable order), i.e. H. it is a canonical representation of the Boolean function ( Bryant , 1986).

By Shannon decomposition Boolean function represented by a binary decision diagram can be calculated. Be of a node of the binary decision diagram. Then the function represented by is defined as

  • if is a leaf, then the function represented is the value of the label of
  • if there is an inner node with label , then is .

example

Representation of a BDD

This picture shows a free, ordered and reduced binary decision diagram. The low edge of a node is shown with a dashed line and the high edge with a solid line. The variable order used is . The function shown can be calculated as follows:

  • -Node:
  • left node:
  • right node:
  • -Node:

We can also evaluate the function shown directly for a given variable assignment. All you have to do is follow the path that belongs to the assignment until you reach a sheet. The value of this sheet is the function value for the given variable assignment.

Let us assume that we want to determine the function value for for the above example . We start at the root of the binary decision diagram. This node is labeled with . Since is in our occupancy , we follow the low edge and reach a node that is labeled. It is true , so we follow the up- edge and reach the sheet with the label 0. Consequently, applies .

Variable orders

The structure and the number of nodes in an ordered and reduced binary decision diagram depend, for many functions, on the selected order of variables. As an example, consider the Boolean function . If you choose the variable order for this, the binary decision diagram needs more than nodes. With the variable order, however, nodes are sufficient .

Binary decision diagram for the function with bad variable order
Good variable order

There are also functions which, regardless of the order of the variables, require an exponential number of nodes in terms of the number of variables. This also includes such important functions as multiplication . Therefore, numerous variants of binary decision diagrams have been developed over the years, 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 made available by all implementations are at least the Boolean operations conjunction (AND), disjunction (OR) and negation (NOT).

The negation can be done by swapping the 0 and 1 leaves of the binary decision diagram. The remaining two-digit Boolean operations are usually traced back to a special ternary operator called the ITE operator:

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

With the help of ITE we can write:

It is easy to convince yourself that all 16 binary Boolean operations can be expressed using the ITE operator. It is therefore sufficient to specify an implementation of the ITE operator.

Other important operations include:

  • Test of two functions shown for equality. Most of the available implementations ensure that nodes that represent the same function are only created once. Then the pointers to the nodes of the binary decision diagram can simply be compared: if they are the same, so are the functions shown and vice versa. The running time is therefore constant (ie ).
  • Test of the feasibility of the function shown, i.e. answering the question of whether the variable is assigned so that the function takes on the value 1. To do this, the binary decision diagram only needs to be compared with the 0-leaf.
  • Calculation of the number of fulfilling assignments: can be done by traversing the binary decision diagram in linear time. For details see [1].

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.
  • BuDDy  : libbdd, a very efficient BDD library, written in C, with a C ++ interface

literature

  • CY Lee . Representation of Switching Circuits by Binary Decision Programs . Bell Systems Technical Journal, 38: 985-999, 1959.
  • Sheldon B. Akers : Binary Decision Diagrams , IEEE Transactions on Computers, C-27 (6): 509-516, June 1978.
  • Randal E. Bryant: Graph-Based Algorithms for Boolean Function Manipulation , IEEE Trans. Computers, Vol. C-35, no. 8 (1986): 677-691.
  • Ingo Wegener : Branching Programs and Binary Decision Diagrams , SIAM Monographs on Discrete Mathematics and Applications 4, ISBN 0-89871-458-3
  • Rolf Drechsler , Bernd Becker: Graph-based function representation. Boolean and pseudo-Boolean functions , Teubner Verlag 1998, ISBN 3-519-02149-8
  • Donald E. Knuth : The Art of Computer Programming - Combinatorial Algorithms, Part 1 , Addison-Wesley 2011, 202-280, ISBN 0-201-03804-8