沿着分支计算函数
布尔决策图，英文简称BDD，是表示布尔函数的有根有向无环图。内部节点询问某个变量的值，分别沿0分支或1分支继续；终端节点给出0或1。对一组确定输入，从根走到终端所得的结果就是函数值。这里的“决策”是逻辑求值，不是机器学习中从样本训练分类器的专用含义。
一个函数可先按变量逐层展开为决策树。若不同分支剩余的判断完全相同，就不必各保存一份。BDD让多个父节点共享同一个子图，因而从树变成图。共享保留了每组输入的答案，并非用近似结果换取较小存储。
有序与简约的两项约束
有序BDD要求所有路径遵守同一个变量先后次序，但路径可以跳过不影响当前结果的变量。进一步简约时有两条规则：一个节点的0、1分支若指向同一子图，就删去这次无效测试；表示相同剩余函数的同构子图只保留一份。通常所说的ROBDD就是满足这些条件的简约有序布尔决策图。
例如f=(x∧y)∨(¬x∧y)，先测试x时，两条分支剩下的函数都是y；合并子图后，x节点的两个后继相同，于是整个图只需测试y。这展示了两条约简规则如何配合，而无需列出四行真值表后逐项比较。
参考：[1]
规范表示能解决什么
Bryant在1986年的研究中系统给出了这种表示及操作算法。固定变量顺序后，一个布尔函数只有一个简约图，忽略节点编号的差别即可。这使函数等价性能够转化为规范图是否相同的比较；但顺序不同的两张图不能直接套用这一结论。
把变量赋值看成状态编码，函数为真的赋值集合就表示一个状态集合。集合的交、并和补可以对应布尔运算；状态转移关系也可用当前状态和后继状态的变量编码。因此符号模型检验可以对状态集合整体操作，而不必把每个状态独立存成记录。规范性有利于判断固定点迭代是否已经稳定。
顺序决定的适用边界
简约并不意味着总能得到小图。比较两组比特是否逐位相等时，交替读取对应的两个比特，所需保留的信息很少；若先读完第一组再读第二组，就可能必须区分第一组的许多不同取值。这类例子说明，变量排序可使表示从小规模增长到指数规模。
还有一些函数无论怎样排序都难以获得紧凑BDD。因此对图的操作很快，不代表从任意短公式构造出的图也一定很小。实际工具会采用排序启发式、共享和缓存，有时动态重排变量；其收益必须结合中间图的规模评估，不能把BDD当成消除所有状态爆炸的通用办法。