Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams

Abstract

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 a wide variety of problems can be solved through symbolic analysis. First, the possible variations in system parameters and operating conditions are encoded with Boolean variables. Then the system is evaluated for all variations by a sequence of OBDD operations. Researchers have thus 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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 1992
Accession Number
ADA253822

Entities

People

  • Randal Bryant

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Algorithms
  • Artificial Intelligence
  • Boolean Algebra
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computer-Aided Design
  • Digital Circuits
  • Formal Languages
  • Hash Tables
  • Logic
  • Logic Gates
  • Mathematical Logic
  • Probability
  • Simulators
  • Trees (Data Structures)

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Artificial Intelligence
  • Graph Algorithms and Convex Optimization.

Technology Areas

  • AI & ML
  • AI & ML - Bayesian Inference
  • AI & ML - Machine Learning Algorithms