An If-then-else Normal Form INF is a Boolean expression built entirely from the ... Each subexpression can be viewed as
An Introduction to Binary Decision Diagrams Henrik Reif Andersen
x
y
y
z
1
0
Lecture notes for 49285 Advanced Algorithms E97, October 1997. (Minor revisions, Apr. 1998) E-mail:
[email protected]. Web: http://www.it.dtu.dk/hra Department of Information Technology, Technical University of Denmark Building 344, DK-2800 Lyngby, Denmark.
1
2
Preface This note is a short introduction to Binary Decision Diagrams. It provides some background knowledge and describes the core algorithms. More details can be found in Bryant's original paper on Reduced Ordered Binary Decision Diagrams [Bry86] and the survey paper [Bry92]. A recent extension called Boolean Expression Diagrams is described in [AH97]. This note is a revision of an earlier version from fall 1996 (based on versions from 1995 and 1994). The major di erences are as follows: Firstly, ROBDDs are now viewed as nodes of one global graph with one xed ordering to re ect state-of-the-art of ecient BDD packages. The algorithms have been changed (and simpli ed) to re ect this fact. Secondly, a proof of the canonicity lemma has been added. Thirdly, the sections presenting the algorithms have been completely restructured. Finally, the project proposal has been revised.
Acknowledgements Thanks to the students on the courses of fall 1994, 1995, and 1996 for helping me debug and improve the notes. Thanks are also due to Hans Rischel, Morten Ulrik S rensen, Niels Maretti, J rgen Staunstrup, Kim Skak Larsen, Henrik Hulgaard, and various people on the Internet who found typos and suggested improvements.
3
CONTENTS
4
Contents 1 2 3 4
Boolean Expressions Normal Forms Binary Decision Diagrams Constructing and Manipulating ROBDDs 4.1 4.2 4.3 4.4 4.5 4.6 4.7
Mk . . . . . . . . . . . . . . . . Build . . . . . . . . . . . . . . Apply . . . . . . . . . . . . . . Restrict . . . . . . . . . . . . SatCount, AnySat, AllSat Simplify . . . . . . . . . . . .
....... ....... ....... ....... ....... ....... Existential Quanti cation and Substitution .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
. . . . . . .
6 7 8 15
15 17 19 20 22 25 25
5 Implementing the ROBDD operations 6 Examples of problem solving with ROBDDs
27 27
7 Veri cation with ROBDDs
31
8 Project: An ROBDD Package References
35 36
6.1 The 8 Queens problem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 6.2 Correctness of Combinational Circuits . . . . . . . . . . . . . . . . . . . . 29 6.3 Equivalence of Combinational Circuits . . . . . . . . . . . . . . . . . . . . 29 7.1 Knights tour . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
CONTENTS
5
1 BOOLEAN EXPRESSIONS
6
1 Boolean Expressions The classical calculus for dealing with truth values consists of Boolean variables x; y; :::, the constants true 1 and false 0, the operators of conjunction ^, disjunction _, negation :, implication ), and bi-implication , which together form the Boolean expressions. Sometimes the variables are called propositional variables or propositional letters and the Boolean expressions are then known as Propositional Logic. Formally, Boolean expressions are generated from the following grammar: t ::= x j 0 j 1 j :t j t ^ t j t _ t j t ) t j t , t; where x ranges over a set of Boolean variables. This is called the abstract syntax of Boolean expressions. The concrete syntax includes parentheses to solve ambiguities. Moreover, as a common convention it is assumed that the operators bind according to their relative priority. The priorities are, with the highest rst: :, ^, _, ,, ). Hence, for example :x ^ x _ x ) x = (((:x ) ^ x ) _ x ) ) x : A Boolean expression with variables x ; : : : ; x denotes for each assignment of truth values to the variables itself a truth value according to the standard truth tables, see gure 1. Truth assignments are written as sequences of assignments of values to variables, e.g., [0=x ; 1=x ; 0=x ; 1=x ] which assigns 0 to x and x , 1 to x and x . With this particular truth assignment the above expression has value 1, whereas [0=x ; 1=x ; 0=x ; 0=x ] yields 0. 1
2
3
4
1
1
1
2
3
4
2
3
4
n
1
3
2
4
1
:
0 1 1 0
^ 0 1
_ 0 1 ) 0 1 0 0 0 0 0 1 0 1 1 1 0 1 1 1 1 1 0 1 Figure 1: Truth tables.
2
3
4
, 0 1 0 1 0 1 0 1
The set of truth values is often denoted B = f0; 1g. If we x an ordering of the variables of a Boolean expression t we can view t as de ning a function from B to B where n is the number of variables. Notice, that the particular ordering chosen for the variables is essential for what function is de ned. Consider for example the expression x ) y. If we choose the ordering x < y then this is the function f (x; y) = x ) y, true if the rst argument implies the second, but if we choose the ordering y < x then it is the function f (y; x) = x ) y, true if the second argument implies the rst. When we later consider compact representations of Boolean expressions, such variable orderings play a crucial role. Two Boolean expressions t and t0 are said to be equal if they yield the same truth value for all truth assignments. A Boolean expression is a tautology if it yields true for all truth assignments; it is satis able if it yields true for at least one truth assignment. Exercise 1.1 Show how all operators can be encoded using only : and _. Use this to argue that any Boolean expression can be written using only _, ^, variables, and : applied to variables. n
2 NORMAL FORMS
7
Exercise 1.2 Argue that t and t0 are equal if and only if t , t0 is a tautology. Is it possible to say whether t is satis able from the fact that :t is a tautology?
2 Normal Forms A Boolean expression is in Disjunctive Normal Form (DNF) if it consists of a disjunction of conjunctions of variables and negations of variables, i.e., if it is of the form (t ^ t ^ ^ t 1 ) _ _ (t ^ t ^ ^ t l ) 1 1
1 2
1
k
l
l
l
1
2
k
(1)
where each t is either a variable x or a negation of a variable :x . An example is j
j
j
i
i
i
(x ^ :y) _ (:x ^ y) which is a well-known function of x and y (which one?). A more succinct presentation of (1) is to write it using indexed versions of ^ and _:
0 1 _ @^j A t : k
l
j i
j =1
i=1
Similarly, a Conjunctive Normal Form (CNF) is an expression that can be written as
0 1 ^ @_j A t l
k
j i
j =1
i=1
where each t is either a variable or a negated variable. It is not dicult to prove the following proposition: Proposition 1 Any Boolean expression is equal to an expression in CNF and an expression in DNF. In general, it is hard to determine whether a Boolean expression is satis able. This is made precise by a famous theorem due to Cook [Coo71]: Theorem 1 (Cook) Satis ability of Boolean expressions is NP-complete. (For readers unfamiliar with the notion of NP-completeness the following short summary of the pragmatic consequences suces. Problems that are NP-complete can be solved by algorithms that run in exponential time. No polynomial time algorithms are known to exist for any of the NP-complete problems and it is very unlikely that polynomial time algorithms should indeed exist although nobody has yet been able to prove their non-existence.) Cook's theorem even holds when restricted to expressions in CNF. For DNFs satis ability is decidable in polynomial time but for DNFs the tautology check is hard (co-NP complete). Although satis ability is easy for DNFs and tautology check easy for CNFs, j i
3 BINARY DECISION DIAGRAMS
8
this does not help us since the conversion between CNFs and DNFs is exponential as the following example shows. Consider the following CNF over the variables x ; : : : x ; x ; : : : ; x : (x _ x ) ^ (x _ x ) ^ ^ (x _ x ) : The corresponding DNF is a disjunction which has a disjunct for each of the n-digit binary numbers from 000 : : : 000 to 111 : : : 111 | the i'th digit representing a choice of either x (for 0) or x (for 1): (x ^ x ^ ^ x , ^ x ) _ (x ^ x ^ ^ x , ^ x ) _ ... (x ^ x ^ ^ x , ^ x ) _ (x ^ x ^ ^ x , ^ x ) : Whereas the original expression has size proportional to n the DNF has size proportional to n2 . The next section introduces a normal form that has more desirable properties than DNFs and CNFs. In particular, there are ecient algorithms for determining the satis ability and tautology questions. Exercise 2.1 Describe a polynomial time algorithm for determining whether a DNF is satis able. Exercise 2.2 Describe a polynomial time algorithm for determining whether a CNF is a tautology. Exercise 2.3 Give a proof of proposition 1. Exercise 2.4 Explain how Cook's theorem implies that checking in-equivalence between Boolean expressions is NP-hard. Exercise 2.5 Explain how the question of tautology and satis ability can be decided if we are given an algorithm for checking equivalence between Boolean expressions. 1 0
1 0
1 1
2 0
1 1
n
0
2 1
n
n
1
n
0
1
i
0
i
1
1 0 1 0
2 0 2 0
n
1 1 1 1
2 1 2 1
n
0
n
0
1
n
1
1
n
1
n
1
1
0 1
n
0
n
1
n
3 Binary Decision Diagrams
Let x ! y ; y be the if-then-else operator de ned by x ! y ; y = (x ^ y ) _ (:x ^ y ) hence, t ! t ; t is true if t and t are true or if t is false and t is true. We call t the test expression. All operators can easily be expressed using only the if-then-else operator and the constants 0 and 1. Moreover, this can be done in such a way that all tests are performed only on (un-negated) variables and variables occur in no other places. Hence the operator gives rise to a new kind of normal form. For example, :x is (x ! 0; 1) , x , y is x ! (y ! 1; 0); (y ! 0; 1). Since variables must only occur in tests the Boolean expression x is represented as x ! 1; 0 . 0
1
0
0
1
1
0
0
1
1
3 BINARY DECISION DIAGRAMS
9
An If-then-else Normal Form (INF) is a Boolean expression built entirely from the if-then-else operator and the constants 0 and 1 such that all tests are performed only on variables. If we by t[0=x] denote the Boolean expression obtained by replacing x with 0 in t then it is not hard to see that the following equivalence holds:
t = x ! t[1=x]; t[0=x] :
(2)
This is known as the Shannon expansion of t with respect to x. This simple equation has a lot of useful applications. The rst is to generate an INF from any expression t. If t contains no variables it is either equivalent to 0 or 1 which is an INF. Otherwise we form the Shannon expansion of t with respect to one of the variables x in t. Thus since t[0=x] and t[1=x] both contain one less variable than t, we can recursively nd INFs for both of these; call them t and t . An INF for t is now simply 0
1
x ! t ;t : 1
0
We have proved:
Proposition 2 Any Boolean expression is equivalent to an expression in INF. Example 1 Consider the Boolean expression t = (x , y ) ^ (x , y ). If we nd an 1
1
2
2
INF of t by selecting in order the variables x ; y ; x ; y on which to perform Shannon expansions, we get the expressions 1
t = t = t = t = t = t = t = t = t = 0 1
00 11
000 001 110 111
x y y x x y y y y
1
1 1 2 2
2 2 2 2
1
2
! t ;t ! 0; t ! t ;0 ! t ;t ! t ;t ! 0; 1 ! 1; 0 ! 0; 1 ! 1; 0 1
2
0
00
11
001
000
111
110
Figure 2 shows the expression as a tree. Such a tree is also called a decision tree. A lot of the expressions are easily seen to be identical, so it is tempting to identify them. For example, instead of t we can use t and instead of t we can use t . If we substitute t for t in the right-hand side of t and also t for t , we in fact see that t and t are identical, and in t we can replace t with t . If we in fact identify all equal subexpressions we end up with what is known as a binary decision diagram (a BDD). It is no longer a tree of Boolean expressions but a directed acyclic graph (DAG). 110
000
00
11
000
110
111
11
1
001
11
00
001
111
3 BINARY DECISION DIAGRAMS
10 x
1
y
y
1
1
x
x
2
2
y
y
2
1
0
y
2
y
2
0
1
0
0
1
2
0
0
1
Figure 2: A decision tree for (x , y ) ^ (x , y ). Dashed lines denote low-branches, solid lines high-branches. 1
1
2
2
Applying this idea of sharing, t can now be written as:
t = t = t = t = t = t = 0 1
00
000 001
x y y x y y
1
1 1 2
2 2
! t ;t ! 0; t ! t ;0 ! t ;t ! 0; 1 ! 1; 0 1
0
00
00
001
000
Each subexpression can be viewed as the node of a graph. Such a node is either terminal in the case of the constants 0 and 1, or non-terminal. A non-terminal node has a low-edge corresponding to the else-part and a high-edge corresponding to the then-part. See gure 3. Notice, that the number of nodes has decreased from 9 in the decision tree to 6 in the BDD. It is not hard to imagine that if each of the terminal nodes were other big decision trees the savings would be dramatic. Since we have chosen to consistently select variables in the same order in the recursive calls during the construction of the INF of t, the variables occur in the same orderings on all paths from the root of the BDD. In this situation the binary decision diagram is said to be ordered (an OBDD). Figure 3 shows a BDD that is also an OBDD. Figure 4 shows four OBDDs. Some of the tests (e.g., on x in b) are redundant, since both the low- and high-branch lead to the same node. Such unnecessary tests can be removed: any reference to the redundant node is simply replaced by a reference to 2
3 BINARY DECISION DIAGRAMS
11
x1 y1
y1 x2
y2
y2
1
0
Figure 3: A BDD for (x , y ) ^ (x , y ) with ordering x < y < x < y . Low-edges are drawn as dotted lines and high-edges as solid lines. 1
1
2
2
1
1
2
2
x1 x1
1
a
x1 x2
x2
1
1
b
c
x3
0
1 d
Figure 4: Four OBDDs: a) An OBDD for 1. b) Another OBDD for 1 with two redundant tests. c) Same as b with one of the redundant tests removed. d) An OBDD for x _ x with one redundant test. 1
3
3 BINARY DECISION DIAGRAMS x y
12
x
