在这节中，我们介绍表示OBDD的经典数据结构和OBDD上的常用操作。
OBDD中每个节点都可用下面这样的一个记录来表示：
type vertex = record
low, high: vertex;
index: 1..n+1;
val: (0,1,X);
id: integer;
mark: boolean;
end
这个记录既可以表示叶子节点，也可以表示非叶子节点，但这两种情况下，记录中各个域的取值是不同的，如表6.2。
| 域 |
low |
high |
index |
val |
| 叶子节点 |
null |
null |
n+1 |
value(v) |
| 非叶子节点 |
low(v) |
high(v) |
index(v) |
X |
其中id域和mark域是以后算法中要用的辅助信息，id域是一个整数，它唯一地标识一个节点，mark域是访问标记。
常用的对BDD的操作有：
(1) 化简（Reduction）：将对任意一种排序的一个BDD简化为OBDD。
(2) 通用逻辑运算（Apply）：在OBDD上定义通用的逻辑运算，如与、或、非。
(3) 限制运算（Restriction）：求给某个变量一个具体的值（0或1）后的OBDD。
(4) 复合运算（Composition）：用一个函数代替一个变量后的OBDD。
(5) 求真集（Satisfy）：求使该函数为真的输入向量集，可求出一条输入向量，也可求出全部满足条件的输入向量。
表6.3中给出以上操作的结果和时间复杂性，|G|表示原BDD的节点数。
| 操作 |
结果 |
时间复杂性 |
| 化简 |
OBDD |
O(|G|log(|G|))
|
| 通用逻辑运算 |
f1<op>f2 |
O(|G1|·|G2|) |
| 复合运算 |
f|xi=b |
O(|G|log(|G|)) |
| |
f1|xi=f2 |
O(|G1|2·|G2|) |
| 求真集 |
一条 |
一条Sf |
O(n) |
| 全部 |
Sf |
O(n·|Sf|) |
| 个数 |
|Sf| |
O(|G|)
|
BDD表示布尔函数的特点如下：
(1) 大部分常用布尔函数的BDD表示都有着可以接受的表示空间。
(2) 布尔函数上的一些常用操作均可以在BDD上通过图遍历算法来实现，且其时间复杂性与BDD的节点数成线性或平方关系。
(3) 用BDD表示布尔函数是正则的，对于给定的一个变量序，功能相同的两个布尔函数的BDD表示是同构的，因此可以很容易判断函数的等价性。这一特点在组合电路的形式验证中发挥着极其重要的作用。
(4) BDD的大小严重依赖于变量的顺序。对于同一函数，不同的变量序其对应的BDD表示空间差别很大。采用启发式算法来求得一个较好的初始变量序，以及用动态调整算法来进行局部优化，是目前常用的两个策略。
|