有序二元决策图 OBDD

决策节点与变量顺序 ​

OBDD 是带两个终端 $0,1$ 的有向无环图公理库有向无环图Directed acyclic graph · DAG不含有向环的有向图。。每个非终端节点标记布尔变量 $x_i$，有 low 边和 high 边，分别对应赋值 $x_i=0,1$。

沿任意根到终端路径，变量必须按照固定全局顺序

$$x_{\pi (1)}<x_{\pi (2)}<\cdots <x_{\pi (n)}$$

出现，变量可以跳过但不能逆序或重复。给定输入赋值，从根按相应边走到的终端就是布尔函数公理库布尔函数Boolean function以有限 Boolean cube 为定义域、输出单个真假值的函数，并区分偏函数、支持变量与限制操作。值。

与决策树公理库决策树模型Decision-tree model · Comparison decision tree用查询节点、答案分支和输出叶刻画算法能够区分输入所需的信息深度。不同，多条路径可以共享同一后缀子图，因此重复子问题只存一次。

两条约简规则 ​

reduced OBDD 反复应用两条规则：若一个节点的 low 与 high 后继相同，删除该冗余节点；若两个节点变量相同且 low/high 后继分别相同，合并这两个同构子图。

在变量顺序固定时，每个布尔函数的 reduced OBDD 在图同构意义下唯一。这一 canonical 性使等价检查化为比较规范根节点，而不必枚举 $2^n$ 个赋值。

规范性依赖“相同变量顺序”和“完全约简”。两个采用不同顺序的图即使表示同一函数，也不能直接按节点身份判等。

XOR 的构造轨迹 ​

取 $f(x,y)=x\oplus y$，顺序 $x<y$。根测试 $x$；若 $x=0$，剩余函数是 $y$；若 $x=1$，剩余函数是 $\mathrm{\neg }y$。

$y$ 节点的 low/high 分别指向 $0,1$，$\mathrm{\neg }y$ 节点则指向 $1,0$。两个节点不能合并，因为后继次序相反。整个图有三个非终端节点和两个共享终端。

若函数是 $(x\wedge y)\vee (\mathrm{\neg }x\wedge y)=y$，初始 Shannon 展开可能生成两个相同 $y$ 子图；合并后根 $x$ 的两条边相同，再删除根，只剩 $y$ 节点。约简真正消除了语法表达式中的冗余。

Apply 与关系运算 ​

给定两个同顺序 OBDD，Apply(op,u,v) 递归对齐两根中较早变量，对 low/high 子对调用自身，再创建或复用唯一节点。memoization 避免同一节点对重复计算。

若输入图大小为 $|G_1|,|G_2|$，最坏访问节点对数为 $O(|G_1||G_2|)$。布尔合取、析取、异或都用该框架；否定可交换终端或逐节点缓存。

存在量化变量 $x$ 可计算为

$$\mathrm{\exists }xf=f[x\leftarrow 0]\vee f[x\leftarrow 1].$$

符号模型检查用量化消除当前/下一状态变量并做变量重命名，完成 predecessor 和 image 运算。

变量顺序的指数风险 ​

OBDD 大小高度依赖变量顺序。相等函数

$$\underset{i=1}{\overset{n}{\bigwedge }}(x_i\leftrightarrow y_i)$$

若按 $x_1,y_1,x_2,y_2,\dots$ 交错，图可保持线性；若先排全部 $x$ 再排全部 $y$，中间必须记住所有 $x$ 赋值，可能指数增长。

动态变量重排常能改善实际图，却有自身时间成本，也不保证找到全局最优顺序。某些函数对每种顺序都需要指数大小，OBDD 不是布尔函数的普遍紧凑编码。

图节点少也不等于公式简单或求值昂贵；表示大小、构造成本和后续 Apply 中间峰值要分开测量。一次操作的中间 BDD 可能远大于最终约简结果。

唯一表与计算表 ​

工程实现用 unique table 保证同一 (variable, low, high) 三元组只对应一个节点，用 computed table 缓存 Apply 的节点对结果。前者维护规范共享，后者避免重复递归；混用两者会让缓存生命周期和垃圾回收出错。节点回收后若旧缓存仍指向复用编号，语义可能被悄悄破坏，因此引用计数或 tracing GC 属于表示正确性的一部分。

终端、变量层级和 complement edges 等编码优化也必须由统一构造入口维护。绕过约简规则手工拼图，即使局部求值看似正确，也会失去 canonical equality 和复杂度假设。

这些表共同维持“相同子函数即相同节点”的实现不变量。

参考资料

• Randal E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Transactions on Computers C-35(8), 1986, pp. 677–691。
• Ingo Wegener, Branching Programs and Binary Decision Diagrams, SIAM, 2000, Chs. 3–6。
• Henrik Reif Andersen, An Introduction to Binary Decision Diagrams, IT University of Copenhagen, 1997。