【模型检测学习笔记】9：Binary Decision Diagrams

1 BDT→\to→BDD→\to→OBDD

在符号模型检测中，用布尔表达式表达一组状态，也就是对布尔公式中的每个变量赋值，可以计算出一个布尔值结果：
f:Booln→Boolf: \ Bool^n \to Boolf: Booln→Bool

所以可以用一个类似于组合解空间树（如果1视为选，0视为不选）的结构，即Binary Decision Tree (BDT) 来表达一个布尔公式，如下图：

图中每个结点vvv有两个孩子分支，一条虚线对应low(v)low(v)low(v)表示v=0v=0v=0，一条实线对应high(v)high(v)high(v)表示v=1v=1v=1。如果不加任何约束，一个布尔公式可以对应多种结构的BDT。

将BDT的所有相同的叶子结点（实际上就只有0和1）合并，就成了Binary Decision Diagram (BDD)。为了保证结构统一，再要求每一层的变量是同一个，即保证所有从根结点到叶子结点的路径上的变量顺序是固定的，就形成了Ordered Binary Decision Diagram (OBDD) ，如下图：

给定一个布尔表达式，从语法层面上来看，可以表示成合取范式（Constructive Normal Form，也称Product of Sum）、析取范式（Disjunctive Normal Form，也称Sum of Product）、电路（Circuit）等；从语义层面上来看，可以表示成真值表（Truth Table）、BDD等。

2 Reduced OBDD

OBDD还可以被约简，考虑两个方面：

合并同构子图，使得没有两个不同的结点有相同的变量（相同的变量在OBDD里只有可能在同一层）以及相同的low(⋅)low(\cdot)low(⋅)和high(⋅)high(\cdot)high(⋅)子结点。对应于ROBDD的性质唯一性（Uniqueness）。
消除冗余，使得没有结点有相同的low(⋅)low(\cdot)low(⋅)和high(⋅)high(\cdot)high(⋅)子结点。对应于ROBDD的性质非冗余测试性（Non-redundant test）。

上面的OBDD合并同构子图后，如下图：

再消除冗余后，得到Reduced Ordered Binary Decision Diagram (ROBDD)，如下图：

大多数时候，BDDs指的就是化简完的ROBDD。对于一个布尔表达式，在给定的变量顺序下，ROBDD是唯一的。使用ROBDD可以在线性时间内做等价性检验（Equivalence Checking），在常数时间内做满足性检验（Satisfiability Checking）。

对于同一个布尔表达式的不同变量顺序下的ROBDD，其复杂程度可能相差非常大，如下图：

寻找最佳的变量顺序是NP难问题。

3 两OBDD上的APPLY运算

给定BϕB\phiBϕ和BψB\psiBψ是两个OBDD，其中ϕ\phiϕ和ψ\psiψ表示它们所表示的布尔表达式，定义两OBDD的APPLY运算：
apply(op,Bϕ,Bψ)apply(op, \ B\phi, \ B\psi)apply(op, Bϕ, Bψ)

其运算结果是对应与布尔表达式ϕopψ\phi \ op \ \psiϕ op ψ的OBDD。

具体计算方法是，从根节点出发，每次找两个OBDD的相对应的path的结果进行op运算，得到的就是新的OBDD上这条path的结果。

4 OBDD上的RESTRICT运算

给定BϕB\phiBϕ是一个OBDD，定义RESTRICT运算：
restrict(0,x,Bϕ)restrict(1,x,Bϕ)restrict(0, \ x, \ B\phi) \\ restrict(1, \ x, \ B\phi) restrict(0, x, Bϕ)restrict(1, x, Bϕ)

其运算结果是对布尔表达式中xxx进行真值指派（ϕ[0/x]\phi[0/x]ϕ[0/x]和ϕ[1/x]\phi[1/x]ϕ[1/x]）得到的新公式的OBDD。

以指派为000为例（111也是类似的），具体计算方法是，对于所有变量是xxx的结点vvv，让其入边直接指向low(v)low(v)low(v)，然后删除结点vvv。

参考阅读

BDD MODEL CHECKING by Loïc Massin