SYMBOLIC BOOLEAN MANIPULATION WITH ORDERED BINARY-DECISION DIAGRAMS

被引：49

作者：

BRYANT, RE

机构：

来源：

COMPUTING SURVEYS | 1992年 / 24卷 / 03期

关键词：

BINARY-DECISION DIAGRAMS; BOOLEAN FUNCTIONS; BOOLEAN ALGEBRA; BRANCHING PROGRAMS; SYMBOLIC ANALYSIS; SYMBOLIC MANIPULATION;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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. 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.

引用

页码：293 / 318

页数：26

共 49 条

[1]

ABELSON H, 1985, STRUCTURE INTERPRETA, P261

[2]

AKERS SB, 1978, IEEE T COMPUT, V27, P509, DOI 10.1109/TC.1978.1675141

[3]

ASHAR P, 1991, OCT P INT C COMP DES, P259

[4]

BEATTY DL, 1991, 28TH P DES AUT C, P397

[5]

BERMAN CL, 1989, OCT P IEEE INT C COM, P392

[6] EQUIVALENCE OF FREE BOOLEAN GRAPHS CAN BE DECIDED PROBABILISTICALLY IN POLYNOMIAL-TIME [J].

BLUM, M ;

CHANDRA, AK ;

WEGMAN, MN .

INFORMATION PROCESSING LETTERS, 1980, 10 (02) :80-82

[7]

BOSE S, 1989, INT C COMPUTER DESIG, P217

[8]

BRACE KS, 1990, P 27 ACM IEEE DES AU, P40

[9]

Brayton R.K., 1984, LOGIC MINIMIZATION A

[10]

BRGLEZ F, 1984, 1984 P INT TEST C, P705

← 1 2 3 4 5 →