Binary Decision Diagrams
By Ammar Alqatari, Michelle McGhee, Michael Vobejda
CS 166 (Data Structures) Final Project
Boolean functions are at the core of many problems in cryptography, complexity theory, computer hardware, and more. Solving these problems efficiently relies on representing these functions clearly and compactly. Binary decision diagrams (BDDs) provide a compact way to uniquely represent a given boolean function.
BDD Basics
BDDs are great because they are canonical and compact.
Let’s say Alice wants to know if she and Bob have equivalent boolean functions. They can’t just send the formulas to each other because even two formulas that look different can actually be equivalent. For a representation to be considered “canonical”, it must be unique — the functions are equivalent if and only if their canonical representations are the same. Unlike boolean formulas, truth tables will provide a unique representation. From a truth table, you can derive a formula’s canonical normal form, which uniquely represents that formula. If two formulas have the same canonical normal form representation, they are equivalent, and vice versa.
Truth tables can get big. A formula with n distinct variables requires 2^n rows to represent its truth table. That means with only 20 variables, you already have millions of rows. Although truth tables are canonical, they are not very compact.
Another way to represent a boolean function is using a binary decision diagram (BDD). A BDD is a rooted, directed, acyclic graph consisting of decision nodes and terminal nodes. The following is a BDD for Alice’s function:
We start with the variable a. The dotted line represents a taking on the value of 0 and the solid line represents a taking on the value of 1. If a = 0, then f will always evaluate to true, so it doesn’t even matter what b is. If b = 0 or if b = 1, it leads to one of the terminal nodes, specifically the 1 terminal. On the other hand, if a = 1, f depends on whether b is 0 or 1, and the two different outcomes are displayed in the branches.
The structure of BBDs are rooted in a mathematical concept called the Shannon expansion. Given a boolean function F of n variables (x1, x2, …, xn), consider the following boolean functions of n-1 variables: F(1, x2, …, xn) and F(0, x2, …, xn). These are referred to as the cofactors of F — the first one is the positive cofactor (the case where x1 = 1) and the second is the negative cofactor (the case where x1 = 0). We can reduce F to a formula of n-1 variables by expanding to consider both of these cases.
A BDD is a visualization of the Shannon expansion of a boolean formula. In the example below, we consider the variable x1. The branches coming out of x1 represent the positive/negative cofactors, the case where x1 = 0 and the case where x1 = 1. Each branching represents a Shannon expansion, until we reach the terminals.
Given a defined variable ordering (in this case, x1 < x2 < x3), both BDDs that we’ve seen are constructed such that in all paths nodes must appear before their children in the variable ordering (a BDD without this restriction is known as a “Free BDD”). This property keeps the diagram organized, but more importantly, it will allow us to do some clever trimming of the BDD.
Even the ordered BDD is somewhat redundant. Let’s look back at the simpler one.
Once we know a = 0, we know that f will evaluate to true no matter what. Perhaps an easier representation would be:
To reduce a BDD, we follow these 2 rules:
1. If a node has two children that are equivalent, we can merge the children into one.
2. If two nodes have the same children, we can merge those nodes into one. We can refer to these nodes as being isomorphic subgraphs.
We can also merge the 0 and 1 terminals into one because it makes it easier to draw. Performing these reduction rules can dramatically reduce the size of the BDD. When a BDD is ordered and reduced, it is known as a Reduced Order BDD (ROBDD). When people refer to BDDs, they are often referring to ROBDDs.
Why are BDDs useful?
BDDs have a number of uses:
- Finding/counting all solutions to a SAT problem — This is the problem of determining whether there exists a variable assignment that satisfies a given boolean formula, or makes it evaluate to true. There is no known algorithm that can efficiently solve every SAT problem, and it has been proven to be NP-complete. BDDs can be used to solve SAT problems (not necessarily efficiently) by constructing the BDD of the formula in question and locating paths that lead to the 1 terminal.
- Equivalence checking — Checking if two boolean formulas are equivalent is easy with BDDs because they are a canonical representation. If the BDDs are the same, the formulas are the same.
An Example: Sudoku
BDDs can be used to solve interesting logic puzzles, like Sudoku. A Sudoku puzzle involves a 9x9 grid, like the one below. The goal is to fill each small box with a number between 1 and 9 such that the entire grid satisfies the following 4 properties:
- Every small box contains exactly one number between 1 and 9.
- Every row contains each number (1–9) exactly once.
- Every column contains each number (1–9) exactly once.
- Each of the 9 outlined 3x3 grids contains each number (1–9) exactly once.
A Sudoku puzzle can be represented as a giant boolean function. Let the variable x_{i, j, k} = 1 if the digit k is chosen for the box at row i, column j in the grid and 0 otherwise. For example, for the solved puzzle above x_{3, 2, 9} = 1 because 9 appears at the spot (3, 2) on the grid. Since i, j, and k all range from 1 to 9, there will be 9³ = 729 of these boolean variables to consider.
Solving the Sudoku puzzle can be seen as assigning 0 or 1 to these boolean variables such that the 3 Sudoku constraints are satisfied. We can take the Sudoku constraints and transform them into a large boolean expression. An assignment of variables that makes that expression true will be the solution to the puzzle.
Note: Reducing the rules to the formulas below was guided by these lecture slides from Aalborg University.
1. Every small box contains exactly one number between 1 and 9.
2. Every row contains each number (1–9) exactly once.
3. Every column contains each number (1–9) exactly once.
4. Each of the 9 outlined 3x3 grids contains each number (1–9) exactly once.
Taking all of these boolean expressions and AND-ing them together produces one huge boolean expression. Whatever variable assignment satisfies this expression is the solution to the puzzle. This is where BDDs come in! If we construct a BDD from the massive boolean expression, we just need to find the paths that lead to the 1 terminal — those are the variable assignments that lead to the expression being true, meaning all the constraints are satisfied.
Implementing a BDD
Guided by Henrik Reif Andersen’s paper “An Introduction to Binary Decision Diagrams”, which explains BDDs theoretically but also outlines their practical implementation, we have implemented a BDD class in C++ that supports the following operations:
- Conjunction
- Disjunction
- SatisfyOne
Using these three operations, we are able to represent and solve boolean functions corresponding to Sudoku puzzles.
Representation
Internally, the BDD is stored as an array of nodes. Each node contains the index of a variable, and two pointers to nodes corresponding to its 0 and 1 assignments. To make sure no duplicate nodes exist in the diagram, the BDD also stores a hash table mapping each node to its index in the array. Whenever a new node is inserted, the hash table is queried to ensure it is unique. Two nodes are considered duplicates if they match in all three attributes: the variable they represent, and their two pointers.
Operations
The two main operations for building BDDs are:
- BUILD(t), which constructs a BDD using a given boolean function t
- APPLY(op, u1, u2), which combines two BDDs u1 and u2 using a boolean operator op, e.g. the and, or operators.
Both operations make use of a function MK which inserts elements uniquely into the diagram by querying the hash table of elements. Coupled with the Shannon expansion, implementing both operations becomes very simple through recursion: BUILD(t) = MK(i, BUILD(t[0\x_i]), BUILD(t[1\x_i]))
Here, t[0\x_i] and t[1\x_i] are the 0 and 1 Shannon cofactors of t, respectively.
Similarly, due to the following relationship, we can recursively implement APPLY:
We can combine the BDDs rooted at u1 and u2 by calling APPLY on their 0 branches together and 1 branches together, then adding them to a common root. Once the terminal nodes are reached, we apply the given operation. We also use memoization to avoid performing the same recursive computations on isomorphic parts of the diagrams. For our Sudoku solver, we use APPLY identically behind the scenes to implement both the Disjunction and Conjunction operators.
Once the BDD is constructed, a variety of variable satisfaction questions can be answered using simple algorithms applied to the BDD. For our application, we implement SatisfyOne, which finds one assignment of the variables which satisfies the given boolean function. With the way the BDD is constructed, SatisfyOne is implemented by simply performing a depth-first search to a 1 terminal node.
With these implementations, BDD operations have the following worst-case runtimes (in expectation, due to constant-time random hashing):
Conclusion
BDDs are a relatively simple, yet powerful data structure that can be used to solve some awesome problems, like Sudoku. They offer a compact way of representing important functions, as well as a step towards solving some of the most significant problems in the world, like SAT. If you like them as much as we do, try implementing them for yourself!
References
- CMU slides about BDD with Sudoku example: http://www.cs.cmu.edu/~emc/15414-f11/lecture/lec05_BDD2.pdf
- Wikipedia article about BDDs: https://en.wikipedia.org/wiki/Binary_decision_diagram
- Donald “God” Knuth on BDDs: https://www.youtube.com/watch?v=axUgEAgrSB8
- More Donald Knuth: https://www.youtube.com/watch?v=SQE21efsf7Y
- Randal Bryant paper: http://www.cs.cmu.edu/~bryant/pubdir/iccad95.pdf
- BDDs and Sudoku: http://people.cs.aau.dk/~kgl/SV-07/Lecture14-3by2.pdf
- Python BDDS library: http://pyeda.readthedocs.io/en/latest/bdd.html
- SAT and BDDs: http://gauss.ececs.uc.edu/Courses/C626/reports/sat_and_bdds.pdf
- Implementing BDDs: http://www.cs.utexas.edu/~isil/cs389L/bdd.pdf
