Graph Based Algorithms for Boolean Function Manipulation12 Randal E Bryant3 Abstract In this paper we present a new data structure for representing Boolean functions and an associated set of manipulation algorithms Functions are represented by directed acyclic graphs in a manner similar to the representations introduced by Lee 1 and Akers 2 but with further restrictions on the ordering of decision variables in the graph Although a function requires in the worst case a graph of size exponential in the number of arguments many of the functions encountered in typical applications have a more reasonable representation Our algorithms have time complexity proportional to the sizes of the graphs being operated on and hence are quite efficient as long as the graphs do not grow too large We present experimental results from applying these algorithms to problems in logic design verification that demonstrate the practicality of our approach Index Terms Boolean functions symbolic manipulation binary decision diagrams logic design verification 1 Introduction Boolean Algebra forms a cornerstone of computer science and digital system design Many problems in digital logic design and testing artificial intelligence and combinatorics can be expressed as a sequence of operations on Boolean functions Such applications would benefit from efficient algorithms for representing and manipulating Boolean functions symbolically Unfortunately many of the tasks one would like to perform with Boolean functions such as testing whether there exists any assignment of input variables such that a given Boolean expression evaluates to 1 satisfiability or two Boolean expressions denote the same function equivalence require solutions to NP Complete or coNP Complete problems 3 Consequently all known approaches to performing these operations require in the worst case an amount of computer time that grows exponentially with the size of the problem This makes it difficult to compare the relative efficiencies of different approaches to representing and manipulating Boolean functions In the worst case all known approaches perform as poorly as the naive approach of representing functions by their truth tables and defining all of the desired operations in terms of their effect on truth table entries In practice by utilizing more clever representations and manipulation algorithms we can often avoid these exponential computations A variety of methods have been developed for representing and manipulating Boolean functions Those based on classical representations such as truth tables Karnaugh maps or canonical sum of products form 4 are quite 1This research was funded at the California Institute of Technology by the Defense Advanced Research Projects Agency ARPA Order Number 3771 and at Carnegie Mellon University by the Defense Advanced Research Projects Agency ARPA Order Number 3597 A preliminary version of this paper was presented under the title Symbolic Manipulation of Boolean Functions Using a Graphical Representation at the 22nd Design Automation Conference Las Vegas NV June 1985 2Update This paper was originally published in IEEE Transactions on Computers C 35 8 pp 677 691 August 1986 To create this version we started with the original electronic form of the submission All of the figures had to be redrawn since they were in a now defunct format We have included footnotes starting with Update discussing some of the minor errors in the original version and giving updates on some of the open problems 3Current address Department of Computer Science Carnegie Mellon University Pittsburgh PA 15213 2 impractical every function of n arguments has a representation of size 2n or more More practical approaches utilize representations that at least for many functions are not of exponential size Example representations include as a reduced sum of products 4 or equivalently as sets of prime cubes 5 and factored into unate functions 6 These representations suffer from several drawbacks First certain common functions still require representations of exponential size For example the even and odd parity functions serve as worst case examples in all of these representations Second while a certain function may have a reasonable representation performing a simple operation such as complementation could yield a function with an exponential representation Finally none of these representations are canonical forms i e a given function may have many different representations Consequently testing for equivalence or satisfiability can be quite difficult Due to these characteristics most programs that process a sequence of operations on Boolean functions have rather erratic behavior They proceed at a reasonable pace but then suddenly blow up either running out of storage or failing to complete an operation in a reasonable amount of time In this paper we present a new class of algorithms for manipulating Boolean functions represented as directed acyclic graphs Our representation resembles the binary decision diagram notation introduced by Lee 1 and further popularized by Akers 2 However we place further restrictions on the ordering of decision variables in the vertices These restrictions enable the development of algorithms for manipulating the representations in a more efficient manner Our representation has several advantages over previous approaches to Boolean function manipulation First most commonly encountered functions have a reasonable representation For example all symmetric functions including even and odd parity are represented by graphs where the number of vertices grows at most as the square of the number of arguments Second the performance of a program based on our algorithms when processing a sequence of operations degrades slowly if at all That is the time complexity of any single operation is bounded by the product of the graph sizes for the functions being operated on For example complementing a function requires time proportional to the size of the function graph while combining two functions with a binary operation of which intersection subtraction and testing for implication are special cases requires at most time proportional to the product of the two graph sizes Finally our representation in terms of reduced graphs is a canonical form i e every function has a unique representation Hence testing for equivalence simply involves testing whether the two graphs match exactly while testing for satisfiability simply involves comparing