企业官网建设流程全解析

二元决策图（BDD, Binary Decision Diagram）发明者故事

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，表示函数值。当变量按固定顺序排列时称为有序BDD（OBDD）；进一步消除冗余节点和合并同构子图后得到简化OBDD（ROBDD），它是布尔函数的唯一规范形式。

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_i=0}) OR (x_i AND f|{x_i=1})。两个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的变量赋值数量（满足赋值计数）。所有操作保持有序性（变量按编号从小到大出现），并通过唯一性表去重以保证规范化。

验收标准表格