Graph-Based Algorithms for Boolean Function Manipulation

Graph-Based Algorithms for Boolean Function Manipulation

June 1985 | Randal E. Bryant
This paper presents a new data structure and algorithms for representing and manipulating Boolean functions using directed, acyclic graphs (DAGs). The representation is similar to those introduced by Lee and Akers, but with additional constraints on the ordering of decision variables. While the worst-case size of the graph is exponential in the number of arguments, many practical functions have more reasonable representations. The algorithms have time complexity proportional to the sizes of the graphs being operated on, making them efficient as long as the graphs do not grow too large. Experimental results show the practicality of this approach in logic design verification. The paper discusses the efficiency of the representation, noting that the size of the graph can be highly sensitive to the ordering of the input variables. Choosing an appropriate ordering is crucial, as poor choices can lead to large graphs. The paper also highlights that some functions, such as those describing integer multipliers, require exponentially growing graphs regardless of input ordering. However, these functions are rare in digital logic design applications. The paper introduces a canonical form for Boolean functions using reduced DAGs, where each function has a unique representation. This allows for efficient equivalence testing and satisfiability checking. The paper also presents algorithms for basic operations on Boolean functions, including reduction, application of operators, and restriction. These algorithms are efficient and can be combined to perform a wide variety of operations on Boolean functions. The reduction algorithm transforms arbitrary graphs into reduced graphs, while the apply algorithm performs operations on functions represented by graphs. The restriction algorithm modifies graphs to represent functions with specific input values. The paper concludes that the proposed methods are efficient and practical for many applications in Boolean function manipulation.This paper presents a new data structure and algorithms for representing and manipulating Boolean functions using directed, acyclic graphs (DAGs). The representation is similar to those introduced by Lee and Akers, but with additional constraints on the ordering of decision variables. While the worst-case size of the graph is exponential in the number of arguments, many practical functions have more reasonable representations. The algorithms have time complexity proportional to the sizes of the graphs being operated on, making them efficient as long as the graphs do not grow too large. Experimental results show the practicality of this approach in logic design verification. The paper discusses the efficiency of the representation, noting that the size of the graph can be highly sensitive to the ordering of the input variables. Choosing an appropriate ordering is crucial, as poor choices can lead to large graphs. The paper also highlights that some functions, such as those describing integer multipliers, require exponentially growing graphs regardless of input ordering. However, these functions are rare in digital logic design applications. The paper introduces a canonical form for Boolean functions using reduced DAGs, where each function has a unique representation. This allows for efficient equivalence testing and satisfiability checking. The paper also presents algorithms for basic operations on Boolean functions, including reduction, application of operators, and restriction. These algorithms are efficient and can be combined to perform a wide variety of operations on Boolean functions. The reduction algorithm transforms arbitrary graphs into reduced graphs, while the apply algorithm performs operations on functions represented by graphs. The restriction algorithm modifies graphs to represent functions with specific input values. The paper concludes that the proposed methods are efficient and practical for many applications in Boolean function manipulation.
Reach us at info@study.space
[slides] Graph-Based Algorithms for Boolean Function Manipulation | StudySpace