有序二叉判定图及其构造算法研究  

The study of ordered binary decision diagram and its constructing arithmetic

作　　者：刘建元[1] 

机构地区：[1]西安邮电学院ASIC中心,陕西西安710061

出　　处：《西安邮电学院学报》2001年第3期6-10,共5页Journal of Xi'an Institute of Posts and Telecommunications

基　　金：国家自然科学基金资助 (6 94730 1)

摘　　要：有序二叉判定图OBDD(orderedbinarydecisiondiagram)是一种数据结构 ,它把布尔函数表示为有向无回路图 ,是布尔函数的一种正则表示 ,可以用来检查布尔函数的一些性质如可满足性、等价性等等。本文将详细地介绍OBDD的数据结构及基于OBDD的布尔函数运算 。Ordered binary decision diagram representing a Boolean function to a directed_acyclic_diagram is a data structure of Boolean function canonical representation . We can check some properties of Boolean function such as satisfiablity, equivalence, ect. This article focuses on data structure of OBDD and operations based on OBDD in detail and reveals arithmetic improved of constructing OBDD.

关 键 词：二叉决策图 分支程序 符号操作 布尔函数 布尔代数 逻辑设计验证 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]