第1章 布尔表达式及其描述 1
1.1布尔函数 1
1.1.1布尔代数 1
1.1.2布尔表达式 3
1.1.3布尔函数 4
1.1.4布尔函数的范式 6
1.2命题公式 8
1.2.1命题与联结词 8
1.2.2合式公式 10
1.2.3命题公式的范式 12
1.2.4命题公式与布尔函数 13
1.3逻辑电路 14
1.3.1基本逻辑门 14
1.3.2逻辑电路的布尔函数 15
1.4布尔表达式的其他描述形式 16
1.4.1真值表 16
1.4.2决策树 17
1.4.3二叉决策图 19
参考文献 21
第2章 有序二叉决策图 22
2.1 OBDD及其规范型 22
2.1.1 OBDD的定义 22
2.1.2 OBDD的性质 23
2.2 OBDD的简化算法 24
2.2.1 OBDD的简化 24
2.2.2简化算法 27
2.3 OBDD的构造及操作 30
2.3.1 OBDD的构造 30
2.3.2 OBDD的操作 31
2.3.3补边OBDD 46
2.4 OBDD的变量序 47
2.4.1 OBDD的最小化 47
2.4.2 OBDD的重排序 49
2.4.3 OBDD的变量序算法 51
参考文献 56
第3章 零压缩二叉决策图 58
3.1 ZBDD及其性质 58
3.1.1组合集合及其表示 58
3.1.2 ZBDD的定义 59
3.1.3 ZBDD的性质 60
3.2 ZBDD的构造及基本操作 61
3.2.1 ZBDD的操作 61
3.2.2 ZBDD的构造 68
3.2.3补边ZBDD 70
3.3.元Cube集合代数 70
3.3.1基本概念 70
3.3.2基本运算 71
3.3.3算法实现 73
3.3.4皇后问题的求解 77
3.4二元Cube集合代数 78
3.4.1二元Cube集的表示 78
3.4.2基本操作及算法 78
3.4.3数字电路设计 83
3.5多项式的隐式表示 85
3.5.1变量次数的表示 85
3.5.2多项式系数的表示 86
3.5.3算术操作的算法实现 87
参考文献 91
第4章 代数决策图 93
4.1 ADD及其性质 93
4.1.1 ADD的定义 93
4.1.2 ADD的矩阵表示 95
4.2 ADD基本操作 96
4.2.1布尔操作 96
4.2.2算术操作 98
4.2.3提取操作 100
4.3矩阵乘法计算 104
4.3.1准环和半环 104
4.3.2半环上的矩阵乘算法 105
4.3.3准环上的矩阵乘算法 108
参考文献 111
第5章 边值二叉决策图 112
5.1 EVBDD及其性质 112
5.1.1 EVBDD的定义 112
5.1.2 EVBDD的规范性 114
5.2操作及其算法 118
5.2.1 Apply操作 118
5.2.2操作的性质 122
5.3整数线性规划求解 126
5.3.1 0-1整数规划求解算法 126
5.3.2改进算法 127
5.3.3 minimize函数 132
5.4函数分解 135
5.4.1函数分解的定义 136
5.4.2无交集函数分解 136
参考文献 138
第6章 二叉矩量图 139
6.1 BMD定义及性质 139
6.1.1函数分解规则 139
6.1.2 BMD的定义 141
6.1.3 BMD的规范性 142
6.1.4*BMD的定义 143
6.1.5 * BMD的构造算法 147
6.2*BMD的操作算法 150
6.2.1整数函数的表示 150
6.2.2 * BMD的加法操作 151
6.2.3*BMD的乘法和幂操作 154
6.2.4布尔函数的表示及操作 157
6.2.5仿射置换 158
6.3算术电路验证 160
参考文献 162
第7章 时间变量决策图 163
7.1差分约束 163
7.1.1差分约束表达式 163
7.1.2差分约束系统 166
7.2差分决策图 169
7.2.1有序差分决策图 169
7.2.2局部简化DDD 171
7.2.3路径简化DDD 172
7.2.4完全简化DDD 177
7.3 DDD的构造及操作 179
7.3.1 DDD的构造 179
7.3.2 RLDDD上的操作 182
7.4赋时二叉决策图 194
7.4.1赋时布尔函数 194
7.4.2赋时布尔函数BDD 197
7.4.3赋时二叉决策图 201
参考文献 202
第8章 应用专题 203
8.1符号模型检验 203
8.1.1计算树逻辑 203
8.1.2 CTL的模型检验 207
8.1.3 CTL的符号模型检验 212
8.2网络优化 215
8.2.1网络最大流问题 215
8.2.2 0-1网络最大流问题的符号算法 217
8.2.3最大流问题的符号算法 222
8.3装配序列规划 228
8.3.1装配序列的符号表示 228
8.3.2装配序列的符号生成 232
8.3.3基于MIPS的装配序列生成 238
8.4 Petri网分析 247
8.4.1基于OBDD的符号分析 247
8.4.2 Petri网调度的符号算法 258
参考文献 264