Symbolic Boolean Manipulation with Ordered Binary-Decision Diagram

This paper has been accepted for publication in ACM Computing Surveys. It was written while on leave at Fujitsu Laboratories, Kawasaki, Japan. This report supersedes report CMU-CS-91-162. Ordered Binary Decision Diagrams (OBDDs) represent Boolean functions as directed acyclic graphs. They form a canonical representation, making testing of functional properties such as satisfiability and equivalence straightforward. In most application, their size remains manageable. A number of operations on Boolean functions can be implemented as graph algorithms on OBDD data structures. Using OBDDs, researchers have solved a number of problems in digital system design, finite state system analysis, artificial intelligence, and mathematical logic. This paper describes the OBDD data structure, and surveys a number of applications that have been solve