本书旨在对有序二叉决策图技术及其应用进行介绍和讨论。全书内容共有8章。第1章对布尔表达式及其描述进行初步介绍，包括布尔函数、命题公式、逻辑电路、布尔表达式的其他描述形式等。第2章讨论有序二叉决策图，包括OBDD及其规范型、OBDD的简化算法、OBDD的构造及操作、OBDD的变量序等。第3章对零压缩二叉决策图进行介绍，包括ZBDD及其性质、ZBDD的构造及基本操作、一元Cube集合代数、二元Cube集合代数、多项式的隐式表示等。第4章介绍代数决策图，包括ADD及其性质、ADD的基本操作、矩阵乘法计算等。第5章对边值二叉决策图进行介绍，包括EVBDD及其性质、操作及其算法、整数线性规划求解、函数分解等。第6章介绍二叉矩量图，包括BMD定义及性质、*BMD的操作算法、算术电路验证等。第7章对时间变量决策图进行介绍，包括差分约束表达式、差分决策图的构造及操作、赋时二叉决策图等。第8章讨论应用专题，包括符号模型检验、网络优化、装配序列规划、Petri网分析等。

有序二叉决策图是布尔函数的一种规范表达形式、一种新型数据结构。基于OBDD可以完成布尔函数的有效表述和操作运算，OBDD在VKSI逻辑综合和验证方面的成功应用引起了学术界和工业应用界的极大关注。本书对OBDD相关技术问题、OBDD扩展形式、OBDD应用等方面进行了介绍和讨沦，主要内容包括布尔表达式及其描述、有序二叉决策网、零压缩二叉决策图、代数决策图、边值二叉决策图、二叉矩量图、时问变量决策图、应用专题等。

本书可供高零院校计算机、电子工程、自动化等专业的高年级本科生、研究生以及相关领域的科研和工程技术人员参考。

前言

第1章 布尔表达式及其描述

 1.1 布尔函数

1.1.1 布尔代数

1.1.2 布尔表达式

1.1.3 布尔函数

1.1.4 布尔函数的范式

 1.2 命题公式

1.2.1 命题与联结词

1.2.2 合式公式

1.2.3 命题公式的范式

1.2.4 命题公式与布尔函数

 1.3 逻辑电路

1.3.1 基本逻辑门

1.3.2 逻辑电路的布尔函数

 1.4 布尔表达式的其他描述形式

1.4.1 真值表

1.4.2 决策树

1.4.3 二叉决策图

 参考文献

第2章 有序二叉决策图

 2.1 OBDD及其规范型

2.1.1 OBDD的定义

2.1.2 OBDD的性质

 2.2 OBDD的简化算法

2.2.1 OBDD的简化

2.2.2 简化算法

 2.3 OBDD的构造及操作

2.3.1 OBDD的构造

2.3.2 OBDD的操作

2.3.3 补边OBDD

 2.4 OBDD的变量序

2.4.1 OBDD的最小化

2.4.2 OBDD的重排序

2.4.3 OBDD的变量序算法

 参考文献

第3章 零压缩二叉决策图

 3.1 ZBDD及其性质

3.1.1 组合集合及其表示

3.1.2 ZBDD的定义

3.1.3 ZBDD的性质

 3.2 ZBDD的构造及基本操作

3.2.1 ZBDD的操作

3.2.2 ZBDD的构造

3.2.3 补边ZBDD

 3.3 一元Cube集合代数

3.3.1 基本概念

3.3.2 基本运算

3.3.3 算法实现

3.3.4 皇后问题的求解

 3.4 二元Cube集合代数

3.4.1 二元Cube集的表示

3.4.2 基本操作及算法

3.4.3 数字电路设计

 3.5 多项式的隐式表示

3.5.1 变量次数的表示

3.5.2 多项式系数的表示

3.5.3 算术操作的算法实现

 参考文献

第4章 代数决策图

 4.1 ADD及其性质

4.1.1 ADD的定义

4.1.2 ADD的矩阵表示

 4.2 ADD基本操作

4.2.1 布尔操作

4.2.2 算术操作

4.2.3 提取操作

 4.3 矩阵乘法计算

4.3.1 准环和半环

4.3.2 半环上的矩阵乘算法

4.3.3 准环上的矩阵乘算法

 参考文献

第5章 边值二叉决策图

 5.1 EVBDD及其性质

5.1.1 EVBDD的定义

5.1.2 EVBDD的规范性

 5.2 操作及其算法

5.2.1 Apply操作

5.2.2 操作的性质

 5.3 整数线性规划求解

5.3.1 0—1整数规划求解算法

5.3.2 改进算法

5.3.3 minimize函数

 5.4 函数分解

5.4.1 函数分解的定义

5.4.2 无交集函数分解

 参考文献

第6章 二叉矩量图

 6.1 BMD定义及性质

6.1.1 函数分解规则

6.1.2 BMD的定义

6.1.3 BMD的规范性

6.1.4 *BMD的定义

6.1.5 *BMD的构造算法

 6.2 *BMD的操作算法

6.2.1 整数函数的表示

6.2.2 *BMD的加法操作

6.2.3 *BMD的乘法和幂操作

6.2.4 布尔函数的表示及操作

6.2.5 仿射置换

 6.3 算术电路验证

 参考文献

第7章 时间变量决策图

 7.1 差分约束

7.1.1 差分约束表达式

7.1 _2差分约束系统

 7.2 差分决策图

7.2.1 有序差分决策图

7.2.2 局部简化DDD

7.2.3 路径简化DDD

7.2.4 完全简化DDD

 7.3 DDD的构造及操作

7.3.1 DDD的构造

7.3.2 RDDD上的操作

 7.4 赋时二叉决策图

7.4.1 赋时布尔函数

7.4.2 赋时布尔函数BDD

7.4.3 赋时二叉决策图

 参考文献

第8章 应用专题

 8.1 符号模型检验

8.1.1 计算树逻辑

8.1.2 CTL的模型检验

8.1.3 CTL的符号模型检验

 8.2 网络优化

8.2.1 网络最大流问题

8.2.2 0—1网络最大流问题的符号算法

8.2.3 最大流问题的符号算法

 8.3 装配序列规划

8.3.1 装配序列的符号表示

8.3.2 装配序列的符号生成

8.3.3 基于MIPs的装配序列生成

 8.4 Petri网分析

8.4.1 基于OBDD的符号分析

8.4.2 Petri网调度的符号算法

 参考文献