二元决策图BDD, Binary Decision Diagram发明者故事081解锁逻辑二元决策图的力量5W1H 故事Who谁有序二元决策图OBDD由 Randal E. Bryant 于1986年在卡内基梅隆大学提出。Bryant在IEEE Transactions on Computers上发表的论文《Graph-Based Algorithms for Boolean Function Manipulation》奠定了现代BDD理论的基础。Donald Knuth在TAOCP第四卷Fascicle 1B中对BDD进行了深入的算法学分析将其纳入组合算法体系。What什么二元决策图BDD是布尔函数的一种规范化有向无环图DAG表示。每个内部节点标记一个布尔变量有两条出边低边lo变量取0时走的路径和高边hi变量取1时走的路径。叶节点为终端节点0或1表示函数值。当变量按固定顺序排列时称为有序BDDOBDD进一步消除冗余节点和合并同构子图后得到简化OBDDROBDD它是布尔函数的唯一规范形式。When何时1986年Bryant发表OBDD论文引发电子设计自动化EDA领域革命。1990年代BDD成为形式验证、模型检测model checking和逻辑综合的核心数据结构。2009年至今Knuth在TAOCP第四卷中系统地将BDD理论整合进组合算法框架。Where何处BDD诞生于美国卡内基梅隆大学计算机科学系随后在Bell实验室、Intel、IBM等工业界被广泛用于硬件验证。现代EDA工具如Cadence、Synopsys中均有BDD模块。Knuth在斯坦福大学的TAOCP工作使BDD的算法学基础更加完备。Why为何布尔函数的真值表表示随变量数指数爆炸无法实用。BDD以紧凑的图结构表示布尔函数支持高效的等价性验证、可满足性计数、逻辑运算等操作。对于许多实际电路函数BDD的规模远小于指数级是形式验证领域的关键突破。How如何BDD构建通过Shannon展开f(x1,…,xn) (NOT x_i AND f|{x_i0}) OR (x_i AND f|{x_i1})。两个BDD的逻辑运算AND/OR/NOT通过递归apply算法实现利用哈希表缓存computed table避免重复计算。节点唯一性通过unique table哈希表保证相同(var, lo, hi)的节点只创建一次。Knuth在TAOCP中还讨论了变量顺序对BDD规模的影响及动态变量重排序算法。自然语言需求定义实现一个简化的有序二元决策图OBDD库支持以下操作使用节点池最多256个节点存储BDD节点每个节点包含变量编号、低边lo和高边hi提供两个预定义终端节点BDD_ZERO和BDD_ONE支持从布尔公式字符串构建BDD支持两个BDD之间的逻辑运算AND、OR及单个BDD的NOT操作支持给定变量赋值对BDD求值支持统计满足当前BDD的变量赋值数量满足赋值计数。所有操作保持有序性变量按编号从小到大出现并通过唯一性表去重以保证规范化。验收标准表格编号测试场景输入期望输出 / 行为验收条件TC-01x1 AND x2的BDD求值赋值x10,x200evaluate返回0TC-02x1 AND x2的BDD求值赋值x11,x211evaluate返回1TC-03x1 OR x2的BDD求值赋值x10,x200evaluate返回0TC-04x1 OR x2的BDD求值赋值x11,x201evaluate返回1TC-05NOT(x1 AND x2)求值赋值x11,x210evaluate返回0TC-06NOT(x1 AND x2)求值赋值x10,x211evaluate返回1TC-07满足赋值计数(x1 OR x2)2个变量3满足赋值数count_solutions返回3TC-08满足赋值计数(x1 AND x2)2个变量1count_solutions返回1TC-09恒真公式BDD_ONEevaluate任意赋值均为1所有4种赋值均返回1TC-10恒假公式BDD_ZEROevaluate任意赋值均为0所有4种赋值均返回0TC-11节点唯一性多次构建相同子公式节点池中无重复节点unique table正常工作