Satisfiability

BDD

An important family of data structures that have uniquely become the method of choice for representing and manipulating Boolean functions inside a computer. The basic idea is a divide-and-conquer scheme somewhat like the binary tries, but with several new twists.

The BDD for a simple Boolean function of three variables, the median function $<x_1,x_2,x_3>$ We can understand it as folows:

• The node at the top is called the root.
• Every internal node, also called a branch node $j$, is labeled with a name or index $1,2,3$ that designates a variable $x_1,x_2,x_3$.
• Branch nodes have two successors, indicated by descending lines. One of the successors is drawn as a dashed line and called LO; the other is drawn as a solid line and called HI.
• These branch nodes define a path in the diagram for any values of the Boolean variables, if we start at the root and take LO branch, when $x_j=0$, the HI branch when $x_j=1$. Eventually this path leads to a sink node, which is either TRUE or FALSE.

Inside a computer, this would be represented by a set of four nodes in arbitrary memory locations, where each node has three fields (V, LO, HI). The V field holds the index of a variable, while the LO and HI fields each point to another node or to a sink:

In essence each BDD is really an abstract set of linked nodes, which might more properly be called a binary decision dag - a binary tree with shared subtrees, a directed acyclic graph in which exactly two distinguished arcs emanate from every nonsink node.

We shall assume that every BDD obeys two important restrictions.

• First, it must be ordered. Whenever a LO or HI arc goes from branch node $i$ to branch node $j$, we must have $i<j$. Thus, in particular, no variable $x_j$ will ever be queries twice when the function is evaluated.
• Second, a BDD must be reduced, in the sense that it doesn’t waste space. This means that a branch node’s LO and HI pointers must never be equal, and that no two nodes are allowed to have the same triple values (V, LO, HI). Every node should be accessible from the root.

Every Boolean function $f(x_1,\dots ,x_n)$ corresponds to a truth table, which is the $2^n$-bit binary string that starts with the function value $f(0,\dots ,0)$ and continuous with $f(0,\dots ,1)$, $f(0,\dots ,0,1,0)$, $f(0,\dots ,0,1,1)$, $\dots$, $f(1,\dots ,1,1,1)$. For example the truth table of the medam function is $00010111$. There’s an important relationship between truth tables and BDDs, which is best understood in terms of binary strings called beads.

A truth table of order $n$ is a binary string of length $2^n$. A bead of order $n$ is a truth table $\beta$ of order $n$ that is not a square; that is, $\beta$ doesn’t have the form $\alpha \alpha$ for any string $\alpha$ of length $2^{n-1}$ There are two beads of order 0, namely 0 and 1; and there are two of order 1, namely 01 and 10. In general there are $2^{2^n}-2^{2^{n-1}}$ beads of order $n$ when $n>0$, because there are $2^{2^n}$ binary strings of length $2^n$ and $2^{2^{n-1}}$ of them are squares.

• order $n$ → length of string $2^n$

• number of truth tables for order $n$ → $2^{2^n}$

• number of beads for order $n$ → $2^{2^n}-2^{2^{n-1}}$

• number of truth tables for order $n$ Boolean function → $1$

• number of beads for order $n$ Boolean function → ??

The beads of a Boolean function are the subtables of its truth table that happen to be beads. For example, again the median function, with its truth table $00010111$. The distinct subtables of this truth table are {00010111, 0001, 0111, 00, 01, 11, 0, 1} and all of them except {00, 11} are beads.

And now we get to the point: The nodes of a Boolean function’s BDD are in one-to-one correspondence with its beads. For example, we can redraw the BDD by placing the relevant bead inside of each node:

The correspondence between beads and nodes proves that every Boolean function has one and only one representation as a BDD. The individual nodes of that BDD might, of course, be placed in different locations inside a computer.

If $f$ is any Boolean function, let $B(f)$ denote the number of beads that it has. That is the size of its BDD - the total number of nodes, including the sinks. For example, $B(f)=6$ when $f$ is the median-of-three function.

Q. Make BDD for a truth table, 1100100100001111:

• The truth table is a bead, so are the two subtables 11001001 and 00001111. Thus we know that the root of its BDD will be $(1)$ branch, and that the LO and HI nodes below the root will be $(2)$s.
• The subtables of length 4 are {1100, 1001, 0000, 1111}; here the first two are beads, but the others are squares.
• To get to the next level, we break the beads in half and carry over the square rots of the nonbeads, identifying duplicates; this leaves us with {11, 00, 10, 01}. Again there are two beads, and a final step produces the desired BDD.
• In this diagram it’s convenient to repeat the sink nodes T and F in order to avoid excessively long connecting lines.

Q. What if the BDD is huge?

Indeed, functions can easily be constructed whose BDD is impossibly huge. But the wonderful thing is that a great many of the Boolean functions that are of practical importance turn out to have reasonably small values of $B(f)$.

If $f(x)=f(x_1,\dots ,x_n)$ is a Boolean function whose BDD is reasonably small, we can do many things quickly and easily.

• We can evaluate $f(x)$ in at most $n$ steps, given any input vector $x=x_1,\dots ,x_n$, by simply starting at the root and branching until we get to a sink.
• We can find the lexicographically smallest $x$ such that $f(x)=1$, by starting at the root and repeatedly taking the LO branch unless it does directly to F. Only $n$ steps are needed, because every branch node corresponds to a nonzero bead; we can always find a download path to T without backing up.
• ,,,
• (so many good things)

Algorithms for solving basic problems with BDDs are often described most easily if we assume that the BDD is given as a sequential list of branch instructions $I_{s-1},I_{s-2},\dots ,I_1,I_0$, where each $I_k$ has the form $({\bar{v}}_k?l_k:h_k)$

Synthesis of BDDs