二元决策图基础

 

译自:An Introduction to Binary Decision Diagrams

作者:Henrik Reif Andersen

 

 

 

 

 

 


 

Efficient Algorithms and Programs, Fall 1999课程笔记

 

电子邮件: hra@itu.dk. 网址: http://www.itu.dk/people/hra

哥本哈根信息技术大学

前言

本讲义是二元决策图Binary Decision Diagrams)的简单介绍,包含一些背景知识和核心算法。更多的细节可以从Bryant最初的无冗降序二元决策图 Reduced Ordered Binary Decision Diagrams)论文[Bry86]以及总览论文[Bry92]中找到。最新的扩展称为布尔表达式图 Boolean Expression Diagrams),可以在[AH97]中找到。

 

本讲义是fall 1996(基于19951994的基础版本)的修正版。主要的变更如下:第一,ROBDD现在被看作全局图(global graph)中的节点,它有固定的变量顺序,且代表了高效BDD包的最高水平。第二,增加了正准性引理canonicity lemma)的证明。第三,重构了讲述算法的章节。第四,改进了项目方案。

 

致谢

感谢fall 199419951996中的学生协助我调试和改进这份讲义。谢谢 Hans Rischel, Morten Ulrik Sørensen, Niels Maretti, Jørgen Staunstrup, Kim Skak Larsen, Henrik Hulgaard, 以及很多网上的朋友帮我改进并找出印刷错误。

 

目录

1. 布尔表达式

2. 范式

3. 二元决策图

4. 构造、操作ROBDD

4.1 Mk

4.2 Build

4.3 Apply

4.4 Restrict

4.5 SatCount, AnySat AllSat

4.6 Simplify

4.7 存在量化和替换

5. 实现ROBDD的指令

6. 实例:用ROBDD解决问题

6.1 八皇后问题

6.2 组合电路的正确性

6.3 组合电路的等价性

7 使用ROBDD验证

7.1 骑士之旅

8 项目:一个ROBDD

Reference

 

1. 布尔表达式

经典的对真值truth value)的演算包括了:a. 布尔变量xy……b. 定值true 1false 0c. 操作符:合取,析取,非¬,蕴涵,双条件。这三种符号组成了布尔表达式。布尔变量也可称作命题变量或者命题字幕。布尔表达式也被称作命题逻辑。

 

布尔表达式用以下规则形式化定义:

 

t ::= x | 0 | 1 | ¬t  |  t ∧ t | t  ∨ t | t  ⇒ t | t  ⇔ t,

 

 

其中,x代表了布尔变量的集合。这称作布尔表达式的抽象语法abstract syntax)。为了解决结合的混淆,具体的语法包含了括号。并且根据传统习惯,所有的操作符都被赋予了优先级。优先级即:按以下顺序优先结合:¬。例如:

 

布尔函数中的x1……xn代表了这个变量的取值是由真值表决定的,见Figure 1真值指派truth assignment)按照顺序把值赋予变量,即:[0/x1, 1/x2, 0/x3, 1/x4]意指将0赋予 x1   x3,将1赋予 xx4。在这种情况下,上边的表达式的值为1[0/x1, 1/x2, 0/x3, 0/x4]将使上边的表达式的值为0

 


真值的集合通常用Β = {0, 1} 表示。如果我们将布尔表达式 的变量次序固定下来,那么我们可以将 t 视为一个由Bn映射向B的函数,其中n代表变量的个数。注意,顺序的选取对于定义该函数而言是非常关键的。思考例子 x⇒y:如果我们的选取的顺序使x<y,那么函数即为f(x,y) =  x⇒y,此情况下第一个参数蕴含了第二个参数使函数为真。如果我们的选取的顺序使x>y,那么函数即为f(y,x) =  x⇒y,此情况下第二个参数蕴含了第一个参数使函数为真。在接下来介绍的布尔表达式的简洁表示中,变量的顺序至关紧要

 

两个布尔表达式  t t' 相等,当且仅当它们在所有的真值指派下,都取相同的真值。当一个布尔表达式在所有的真值指派下都为真,那么它被称作重言式tautology,又叫永真式)。当一个布尔表达式至少在一种真值指派下为真,那么它被称为可满足的satisfiable)。

 

练习 1.1 ¬表示所有其他的逻辑操作符。以此证明所有的布尔表达式都可仅用¬和变量表达。

练习 1.2 证明: t t' 相等当且仅当 t t' 为重言式。是否可证当  ¬t为重言式时, t为可满足的。

 

2. 范式

如果一个布尔表达式只由变量的合取和变量的否定的析取组成,那么它为析取范式DNFDisjunctive Normal Form)。即,如果它由如下形式构成

 


且每一个都是变量或者其否定形式。例如下面是一个非常有名的函数(异或):

 


(1)更简明的表示为:

 


相同的,合取范式CNFConjunctive Normal Form)可写作:

 


其中均为变量或者变量的否定。则不难推出命题:

 

命题1 任何布尔表达式都可以表示为CNF或者DNF

 

一般地,一个布尔表达式是否是可满足的很难识别。Cook对此有一个著名的定理[Coo71]

 

定理1 Cook 布尔表达式的可满足性为NP-complete

 

(对于不熟悉NP-completeness概念的读者,可以看下面的总结:NP-complete的问题可以用指数时间exponential time)的算法解决。没有已知的多项式时间polynomial time)的算法可以解决任意一个NP-complete的问题,而且也很难证明有这样的多项式时间的算法存在。虽然如此,也没有人可以证明这样的算法不存在。)

 

Cook定理甚至对CNF也有效。DNF可满足性问题可由多项式时间的算法计算,但是DNF的恒真检查是很难的(co-NP complete)。尽管可满足性之于DNF,恒真检查之于CNF都是容易的,这对我们帮助不大:CNFDNF的转换是指数时间的,以下例子可以说明这个问题。

考虑由变量构成的CNF:

 


相应的DNF是一个从000…000111…111n位二进制数的析取,其中第i位代表了选取还是:

 


当原表达式的大小与n成正比时,DNF则与n2n成正比。

 

下一节介绍了比DNFCNF更可取的范式。特别是对于可满足性问题和恒真问题有极其有效的算法。

 

练习 2.1 描述一个判断DNF是否为可满足的多项式时间算法。

练习 2.2 描述一个判断CFN是否为恒真的多项式时间算法。

练习 2.3 证明命题1

练习 2.4 解释Cook定理是如何证明判断两个布尔表达式是否不等价是NP-hard的。

练习 2.5 解释为什么给出一个检查两个布尔表达式等价性的算法,则恒真和可满足性是可判断的。

 

3. 二分决策图

让形如x→y0,y1称作一个if-then-else操作符,其定义为:


这样对于t→t0,t1,当tt0为真,或者t为假,t1为真时,该表达式为真。t被称为测试表达式test expression)。所有的操作符都可以仅用if-then-else操作符以及01表示。这可由将所有的测试由(非否定形式的)变量和没有在其他地方出现的变量的方式达成。这样就构成了一种新的范式。例如,¬x即是(x→0,1)x⇔y即是x→(y→1,0),(y→0,1)。因为所有的变量都要出现在测试表达式里,所以x应表示为 x→1,0

 

一个IF判断范式If-then-else Normal Form, INF)是一个完全只由if-then-else操作符和01构成的布尔表达式,其中的测试只在变量上进行。

 

 

如果我们用 t[0/x]代表将布尔表达式t中的所有变量x0取代,那么易得:

 


这被称为t关于x香农扩展Shannon Expansion。这一个简单的等式有很多有用的应用。第一个应用是从任何表达式t中生成INF。如果t不包含任何变量,那么t要么是0,要么是1,这两种形式都是INF。否则我们可以生成t关于任一x的香农扩展。这样无论t[0/x]还是t[1/x]都比t少一个变量。我们可以递归地从这两者中找到INF;称他们t0t1。这样一个tINF为:x→t0,t1

 

已证明:

 

命题2 任何布尔表达式都与一个INF形式的表达式等价。

 

1 考虑布尔表达式t = (x1⇔y1)∧(x2⇔y2)。如果我们可以找到一个tINF,且指定变量的顺序:x1y1x2y2,通过香农扩展,我们可以获得以下表达式:

 


 

Figure 2将此表达式展示为一个书。这样的树也被称为决策树。

 

许多表达式可以轻易地证明完全相同,所以找出它们是一件很诱人的工作。例如,我们可以用t000代表t110,用t001代表t111,如果我们用t000取代t11右边的t110,同样地用t001取代t11右边的t111,可以发现t00t11是完全相同的。所以可以在t1中用t00取代t11

 

如果我们可以找出所有相等的子表达式,并把它们全都简化,我们即可获得一个二元决策图binary decision diagramBDD)。它不再是一个布尔表达式构成的树,而是一个有向无环图directed acyclic graphDAG)。

 


 

由共享子树出发,我们可以将t写成:

 


 

每一个子表达式都可视作图的一个节点。这样一个节点要么是01汇聚节点,要么就是有后继的分支节点。(译者注,为了与《计算机程序设计艺术(第四卷)》一书统一,本文的terminal译为汇聚节点sink nodenon-terminal译为分支节点branch node。然而,《计算机程序设计艺术(第四卷)》中还有根节点的概念。本文并未突出根节点有何特殊性,所以可以一概而论。)分支节点有一个低分支low-edgeLO),相关于表达式的else部分;和一个高分支high-edgeHI),代表了then部分,如Figure 3。注意,节点的数目,从决策树中的9,降低到了BDD中的6。不难想象,如果分支节点是一个其他巨大的决策树,那么就会节省非常客观的数目。因为在递归构建tINF中,我们以约定的顺序选取了变量,变量以同样的顺序出现在了从根节点出发的BDD中。所Figure 3展示的BDD也是OBDD

 


Figure 4展示了四个OBDD。一些测试(例如图b中的x2)是冗余的,因为HILO都指向了相同的节点。这样的不必要的测试可以移除:所有这样冗余的节点,都将直接指向其子节点的线段代替。如果所有的相同节点都是共享的,所有的冗余测试都将被移除,那么这个OBDD则称为已约化的reduced)。这样的一个OBDD即为ROBDDROBDD有非常多有用的性质。这些性质的核心是下面的正准性引理canonicity lemma)。(大部分情况下使用BDD这个词,都是在讨论ROBDD)。

 


 

以上内容总结如下:

BDD是一个有根节点的,有向无环图,且有:

         120出度out-degree)的汇聚节点,01,且有

         一个出度为2的分支节点u的集合。两个向外的边分别由low(u)high(u)给出。(在图中,分别由虚线和实线表式。)一个变量var(u)相关于此节点。

BDD是有序的,当且仅当图中所有的路径经过的变量都遵循一个给定的线性序 x1< x2<...< xn (O)BDD是已约化的,当且仅当:

         唯一性uniqueness)没有两个相同的节点uv绑定了相同的变量,且有相同的LOHI后继,即:var(u) = var(v), low(u) = low(v), high(u) = high(v)可得u = v,且

         无冗余测试non-redundant tests)没有任何一个节点u有相同的LOHI后继,即:low(u) high(u)

 

Figure 5展示了有序性和已约化性。

 

 


 

ROBDD 有很多有趣的性质。它们提供了一个简洁的布尔表达式的表示方式,并且所有的ROBDD的逻辑操作都有快速算法。这些都基于这样一个事实:对于每一个函数f : BnB,有且仅有一个ROBDD与之对应。这意味着,有且仅有一个ROBDD代表恒真和恒假:汇聚节点10。因此,检验一个ROBDD是否恒真或恒假(可能)有常数时间的方法。(对于布尔表达式,这个问题是NP-complete的。)

 

为了更详细的解释,我们必须说明用ROBDD表示函数的意义。第一,很容易发现ROBDD的节点是如何归纳地定义布尔表达式tu的:汇聚节点表示布尔常数(01)。用x标示的分支节点是一个if-then-else表达式,其测试条件为x,其两个分支为LOHI给出的布尔表达式。形式化定义如下:

 

t0 = 0

t1 = 1

tu = var(u) → thigh(u), tlow(u), u为布尔变量节点。

 

如果x1 < x2 < … < xn ROBDD的变量顺序,我们将每一个节点u相关于函数fufu(b1, b2, …, bn) Bn映射至tu [b1/x1 , b2/x2, …, bn/xn]的真值。我们可以得到关键的引理:

 

引理 1 正准性引理,Canonicity lemma

对于任意函数f : BnB,有且仅有一个变量顺序为x1 < x2 < … < xn ROBDD u,如fu = f(x1 , x2 , … , xn)

 

证明:

证明过程为对f参数数量的归纳:

 

(1) 对于n=0,有且仅有两个布尔函数:恒真函数,恒假函数。因为任何ROBDD都有至少一个分支节点是非常量。因此这两个函数都分别对应一个ROBDD:汇聚节点:10

 

(2)假设:已证引理1n个参数下成立。

 

那么在n+1个参数时,使f : Bn+1 B为任意n+1个参数的布尔函数。定义两个函数f0f1n个参数的函数,其由函数f把第一个参数分别改为01得出:

 

fb( x2 , … , xn) = f(b,  x2 , … , xn) b B

 

(有时f0f1称为f关于x1负协函子negative co-factor)正协函子positive co-factor))这两个函数构成了如下等式:

 

f(x1 , x2 , … , xn) = x1 f1( x2 , … , xn),  f0( x2 , … , xn) (3)

 

因为f0f1都只需要n个参数,根据假设,有唯一的ROBDD节点u0u1构成fu0 = f0fu1 = f1

 

这有两种情况:

(2.1) 如果u0 = u1,那么fu0 = fu1 ,且f0 = fu0 =  fu1 = f1 = f。因此 u0 = u1即为fROBDD。根据变量顺序,这也是f的唯一ROBDD。如果x1已经存在于以u为根节点的ROBDD中,x1应该为根节点。然而,如果 f = fu,那么f0 = fu[0/x1] = flow(u)f1 = fu[1/x1] = fhigh(u)。因为f0 =fu0 =  fu1 = f1,左右分支是相同的,这与ROBDD无冗余测试性质相悖。(此情况为x1 的取值对于函数取值没有影响。这说明该函数对应的ROBDD就是省略掉 x1之后的n参数的函数f0f1ROBDD,译者注)

(2.2) 如果u0 u1,那么可以从归纳假设中得到fu0 fu1 (使用  x2 , … , xn+1 代替 x1 , … , xn)。使uvar(u) = x1 low(u) = u0 high(u) = u1的节点。也就是fu = x1 fu1 ,fu0 ,它是已约化的。

通过假设fu0 = f0   fu1 = f1,根据式(3),可以推断出 fu = f。假设v是一个其他的节点且 fv = f,很明显,fv 一定依赖于x1,也就是说fv [0/x1] fv [1/x1] (否则f0 = fv[0/x1] = fv[1/x1]  = f1,与假设矛盾)。因为有序性,这意味着var(v) = x1 = var(u)。而且,从 fv = f 可以得出, flow(v)  = f= fu0 fhigh(v)  = f= fu1 ,根据假设low(v) = u0 = low(u) high(v) = u1 =high(u)。根据已约化性质,u = v

 

重要的结论如下:汇聚节点1是对于任何变量顺序,唯一为恒真的ROBDD。判断ROBDD是不是汇聚节点1可用常数时间的操作判断。这对恒假同样成立。实际上,判断两个布尔函数是否相同,可以通过在同一个图中构造它们的ROBDD,然后检查他们的节点是否相同。

 

ROBDD的变量顺序对于其大小的影响非常大。考虑表达式:(x1⇔y1)∧(x2⇔y2)然后以x1 < x2 < y1 < y2 的顺序构造ROBDD Figure 6),那么将有9个节点。Figure 3中的ROBDD只有6个节点。

 


练习 3.1 if-then-else操作和01表示所有的操作符。

练习 3.2 以顺序x1 < y1 < x2 < y2 < x3 < y3 x1 < x2< x3 < y1 < y2 < y3(x1⇔y1)∧(x2⇔y2)∧(x3⇔y3)ROBDD

练习 3.3 x1 < x2 < y1 < y2 x1 < y1 < x2 < y2 的顺序画(x1⇔y1)∨(x2⇔y2)ROBDD。它们与 Fiugre 3 Figure 6 有何不同?根据这些例子,什么顺序可以为(x1⇔y1)∧(x2⇔y2)∧(x3⇔y3)∧…∧(x3⇔y3) 生成较小的ROBDD

练习 3.4 举例一系列的ROBDD un 0 ≤ n),它们使决策树指数式增长。也就是说,un的大小为θ(n)的话,其决策树为θ(2n)

练习3.56个变量构造最大的ROBDD

41个节点? 1+2+4+6+16+8+2

 

4. 构造、操作ROBDD

在上一节,我们了解了如何通过一个简单的递归过程使用布尔表达式构造OBDD。现在考虑如何构造无冗的OBDD。一个简单的方式是先构造OBDD,再进行简化。另外一个有效的方法为,在构造中简化OBDD。下面将作详细解释。

 

为了描述这个过程,我们需要指出一种ROBDD的表示方式。节点由数字0, 1, 2, ...表示,01保留为汇聚节点。

4.1 Mk

4.2 Build

4.3 Apply

4.4 Restrict

4.5 SatCount, AnySat AllSat

4.6 Simplify

4.7 存在量化和替换

5. 实现ROBDD的指令

6. 实例:用ROBDD解决问题

6.1 八皇后问题

6.2 组合电路的正确性

6.3 组合电路的等价性

7 使用ROBDD验证

7.1 骑士之旅

8 项目:一个ROBDD

本项目将实现一个包含ROBDD操作的简易包。整个包应该包含以下操作:

 

Init(n)

初始化包。使用从1nn个变量。

Print(u)

在标准输出中打印ROBDD。这对Debug非常有用。

Mk(i,l,h)

返回一个节点的编号u,其中var(u)  =ilow(u) = lhigh(u) = h。这个可能是一个已有的节点,或者一个新建的节点。这个操作要注意不要违反了ROBDD的约化性。

Build(t)

从一个布尔表达式中建立ROBDD。你可以专注于表达式x¬x,或者它们的合取。(为什么?)

Apply(op,u1,u2)

构造将op应用于u1u2ROBDD

Restrict(u,j,b)

通过真值指派[b/xj],限定ROBDD u

SatCount(u)

返回集合sat(u)中的元素数量。(用一个可以包含非常大的数的类型,如浮点数。)

AnySat(u)

返回一个符合要求的u的真值指派。

 

子项目 1

实现第四节中的表TH以及它们的操作。在这之上,实现操作Init(n)Print(u)Mk(i,l,h)

子项目 2

继续添加操作Build(t)Apply(op,u1,u2)

子项目 3

添加操作Restrict(u,j,b)SatCount(u)AnySat(u)

 

Reference

 

[AH97]

 

Andersen, Henrik Reif, and Henrik Hulgaard. "Boolean expression diagrams." Logic in Computer Science, 1997. LICS'97. Proceedings., 12th Annual IEEE Symposium on. IEEE, 1997.

 

Link: http://www.sciencedirect.com/science/article/pii/S0890540101929487/pdf?md5=aa1c74f8d5af7f06b028376d6c6af645&pid=1-s2.0-S0890540101929487-main.pdf

 

[Bry86]

 

Bryant RE. Graph-based algorithms for boolean function manipulation. Computers, IEEE Transactions on. 1986 Aug;100(8):677-91.

 

Link: https://pdfs.semanticscholar.org/f5c1/b943517eabf5ef33d95d922f1343e88960d0.pdf

 

[Bry92]

 

Bryant RE. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys (CSUR). 1992 Sep 1;24(3):293-318.

 

Link: http://www.di.ens.fr/~jv/HomePage/dea/bryantonBDD.pdf

 

 

[CBM89]

 

Coudert O, Berthet C, Madre JC. Verification of synchronous sequential machines based on symbolic execution. InInternational Conference on Computer Aided Verification 1989 Jun 12 (pp. 365-373). Springer, Berlin, Heidelberg.

 

Link: https://link.springer.com/chapter/10.1007/3-540-52148-8_30

 

[CLR90]

 

Cormen TH. Introduction to algorithms. MIT press; 2009 Jul 31.

 

Link: http://ressources.unisciel.fr/.../%5BCormen-AL2011%5DIntroduction_To_Algorithms-A3.pdf

 

[Coo71]

 

Cook SA. The complexity of theorem-proving procedures. InProceedings of the third annual ACM symposium on Theory of computing 1971 May 3 (pp. 151-158). ACM.

 

Link: https://www.cs.toronto.edu/~sacook/homepage/1971.pdf

 

[Mil89]

 

Milner R. Communication and concurrency. New York etc.: Prentice hall; 1989 Jan 3.

 

Link: https://www.goodreads.com/book/show/788766.Communication_and_Concurrency

档铺网——在线文档免费处理