Editing Binary decision diagram (section)

== Definition ==
A Boolean function can be represented as a [[Rooted graph|rooted]], directed, acyclic [[graph theory|graph]], which consists of several (decision) nodes and two terminal nodes. The two terminal nodes are labeled 0 (FALSE) and 1 (TRUE). Each (decision) node <math>u</math> is labeled by a Boolean variable <math>x_i</math> and has two [[child node]]s called low child and high child. The edge from node <math>u</math> to a low (or high) child represents an assignment of the value FALSE (or TRUE, respectively) to variable <math>x_i</math>. Such a '''BDD''' is called 'ordered' if different variables appear in the same order on all paths from the root. A BDD is said to be 'reduced' if the following two rules have been applied to its graph:
* Merge any [[Graph isomorphism|isomorphic]] subgraphs.
* Eliminate any node whose two children are isomorphic.

In popular usage, the term '''BDD''' almost always refers to '''Reduced Ordered Binary Decision Diagram''' ('''ROBDD''' in the literature, used when the ordering and reduction aspects need to be emphasized). The advantage of an ROBDD is that it is canonical (unique up to isomorphism) for a particular function and variable order.<ref name="Bryant1986"/> This property makes it useful in functional equivalence checking and other operations like functional technology mapping.

A path from the root node to the 1-terminal represents a (possibly partial) variable assignment for which the represented Boolean function is true. As the path descends to a low (or high) child from a node, then that node's variable is assigned to 0 (respectively 1).

=== Example ===
The left figure below shows a binary [[decision tree|decision ''tree'']] (the reduction rules are not applied), and a [[truth table]], each representing the function <math>f(x_1, x_2, x_3)</math>. In the tree on the left, the value of the function can be determined for a given variable assignment by following a path down the graph to a terminal. In the figures below, dotted lines represent edges to a low child, while solid lines represent edges to a high child. Therefore, to find <math>f(0, 1, 1)</math>, begin at x<sub>1</sub>, traverse down the dotted line to x<sub>2</sub> (since x<sub>1</sub> has an assignment to 0), then down two solid lines (since x<sub>2</sub> and x<sub>3</sub> each have an assignment to one). This leads to the terminal 1, which is the value of <math>f(0, 1, 1)</math>.

The binary decision ''tree'' of the left figure can be transformed into a binary decision ''diagram'' by maximally reducing it according to the two reduction rules. The resulting '''BDD''' is shown in the right figure.

{| align="center"
|-
| [[File:BDD.png|thumb|546px|Binary decision tree and [[truth table]] for the function <math>f(x_1, x_2, x_3)=(\neg x_1 \wedge \neg x_2 \wedge \neg x_3) \vee (x_1 \wedge x_2) \vee (x_2 \wedge x_3)</math>, described in notation for [[Boolean algebra#Basic operations|Boolean operators]].]]
| [[File:BDD simple.svg|thumb|189px|BDD for the function ''f'']]
|}

Another notation for writing this Boolean function is <math>\overline{x}_1 \overline{x}_2 \overline{x}_3 + x_1 x_2 + x_2 x_3</math>.

=== Complemented edges ===
[[File:BDD diagram with complemented edges 2.png|thumb|Representation of a binary decision diagram using complemented edges|287x287px]]

An ROBDD can be represented even more compactly, using complemented edges, also known as ''complement links''.<ref name="Brace"/><ref name="Somenzi1999"/> The resulting BDD is sometimes known as a ''typed BDD''<ref name="MB88"/> or ''signed BDD''.
Complemented edges are formed by annotating low edges as complemented or not. If an edge is complemented, then it refers to the negation of the Boolean function that corresponds to the node that the edge points to (the Boolean function represented by the BDD with root that node). High edges are not complemented, in order to ensure that the resulting BDD representation is a canonical form. In this representation, BDDs have a single leaf node, for reasons explained below.

Two advantages of using complemented edges when representing BDDs are:
* computing the negation of a BDD takes constant time
* space usage (i.e., required memory) is reduced (by a factor at most 2)
However, Knuth<ref name="Knuth"/> argues otherwise:
:''Although such links are used by all the major BDD packages, they are hard to recommend because the computer programs become much more complicated. The memory saving is usually negligible, and never better than a factor of 2; furthermore, the author's experiments show little gain in running time.''

A reference to a BDD in this representation is a (possibly complemented) "edge" that points to the root of the BDD. This is in contrast to a reference to a BDD in the representation without use of complemented edges, which is the root node of the BDD. The reason why a reference in this representation needs to be an edge is that for each Boolean function, the function and its negation are represented by an edge to the root of a BDD, and a complemented edge to the root of the same BDD. This is why negation takes constant time. It also explains why a single leaf node suffices: FALSE is represented by a complemented edge that points to the leaf node, and TRUE is represented by an ordinary edge (i.e., not complemented) that points to the leaf node.

For example, assume that a Boolean function is represented with a BDD represented using complemented edges. To find the value of the Boolean function for a given assignment of (Boolean) values to the variables, we start at the reference edge, which points to the BDD's root, and follow the path that is defined by the given variable values (following a low edge if the variable that labels a node equals FALSE, and following the high edge if the variable that labels a node equals TRUE), until we reach the leaf node. While following this path, we count how many complemented edges we have traversed. If when we reach the leaf node we have crossed an odd number of complemented edges, then the value of the Boolean function for the given variable assignment is FALSE, otherwise (if we have crossed an even number of complemented edges), then the value of the Boolean function for the given variable assignment is TRUE.

An example diagram of a BDD in this representation is shown on the right, and represents the same Boolean expression as shown in diagrams above, i.e., <math>(\neg x_1 \wedge \neg x_2 \wedge \neg x_3) \vee (x_1 \wedge x_2) \vee (x_2 \wedge x_3)</math>. Low edges are dashed, high edges solid, and complemented edges are signified by a circle at their source. The node with the @ symbol represents the reference to the BDD, i.e., the reference edge is the edge that starts from this node.