二元决策图（BDD）

二元决策图简称BDD,是一种表示布尔函数的图状数据结构。它把函数展开成一棵二叉决策树,再通过合并等价子图和删除冗余节点将其压缩成有向无环图,从而在许多情况下极大节省空间。

概述

直接用真值表表示n变量布尔函数需要指数大小的空间,而BDD通过共享结构常能得到紧凑表示。布莱恩特在一九八六年提出的有序规约二元决策图尤为重要,它固定变量测试顺序并施加规约规则,使每个函数拥有唯一的规范表示。

核心特点

• 每个内部节点对应一个变量,引出低边和高边分别表示该变量取零和取一。
• 叶节点只有代表真和假的两个终端。
• 有序性要求所有路径上变量按同一顺序出现。
• 规约规则要求删除两条子边指向同一节点的冗余节点,并合并结构完全相同的子图。
• 在固定变量序下,规约有序BDD是布尔函数的唯一规范形式。

应用场景

BDD是形式化验证和电路设计自动化的关键工具。它被用于组合电路和时序电路的等价性检查、符号模型检测中状态集合的紧凑表示、可满足性判定以及可靠性分析。由于规范性,判断两个布尔函数是否相等只需比较它们的BDD是否为同一个图。

常见问题

问:变量顺序对BDD有多大影响?答:影响极大。同一函数在不同变量序下的BDD大小可能相差指数级,寻找最优变量序本身是难解问题,因此实践中依赖启发式排序。

问:为什么BDD能判断布尔函数相等?答:因为在固定变量序下规约有序BDD是唯一规范形式,两个函数相等当且仅当它们对应完全相同的BDD,这使等价性检查退化为简单的图比较。