posted on 1966-01-01, 00:00authored byRandal E. Bryant
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.