Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams

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 solved by OBDD-based symbolic analysis.