（计算机应用技术专业论文）二元决策图的排序优化及故障树转化方法的研究.pdf

摘要 随着计算机软硬件系统日益复杂，保证系统的正确性和可靠性日 显重要，为此提出的许多理论和方法中，模型检测以其简洁明了和自 动化程度高而引人注目。 论文介绍了二元决策图的基本原理与研究现状，针对影响二元决 策图结构的因素变量排序进行了深入分析；给出了节点规模优化 的排序算法的改进思想；研究了利用动态交换来完成路径数量优化的 方法，提出了o s m n p 排序优化算法。该算法通过对节点路径的定义 和记录，实现了在变量交换中局部路径改变量向全局改变量的转移， 从而实现路径数量的优化。论文还研究了基于二元决策图的故障树分 析的排序和转化问题，提出一种快速有效的l n p c 方法，该方法采用 逐渐分解的策略直接完成子事件的排序与组合，一次性地实现故障树 n - 元决策图的转化与优化，并通过实例验证了其有效性。 o s m n p 算法利用相邻变量交换的有效性能获取最少路径的排 序；l n p c 算法通过按定义的规则遍历故障树不仅完成底事件的优化 排序，同时也有效地实现了故障树向二元决策图的转化，这些研究成 果对二元决策图应用的深入有较好的理论意义和一定的实用价值。 关键词二元决策图，有序二元决策图，节点，路径，排序优化， 故障树 a b s t r a c t w i t ht h ei n c r e a s i n gc o m p l e x i t yo fc o m p u t e rh a r d w a r ea n ds o f t w a r e s y s t e m st oe n s u r et h ea c c u r a c ya n dr e l i a b i l i t y o fs y s t e m s ，a n dm o r e i m p o r t a n t ，f o rt h em a n yt h e o r i e sa n dm e t h o d so fd e t e c t i o nm o d e lw i t hi t s c l e a r ，c o n c i s ea n dah i g hd e g r e eo fa u t o m a t i o na n da t t e n t i o n p a p e r so nt h eb i n a r yd e c i s i o nd i a g r a ma n ds t u d yt h eb a s i cp r i n c i p l e s o ft h es t a t u sq u o ，a g i n s ta f f e c t i n gf a c t o r so ft h es t r u c t u r e - 一v a r i a b l es o r t c o n d u c t e di n d e p t ha n a l y s i s ，a ni m p r o v i n gi d e at h a t o p t i m i z et h es c a l eo f n o d eo fb d di sp r o p o s e d r e s e a r c ho nt h eu s eo fd y n a m i ce x c h a n g et o c o m p l e t et h ep a t h o p t i m i z a t i o no ft h en u m b e ro fm e t h o d sp r o p o s e d o s m n ps o r to p t i m i z a t i o n t h ea l g o r i t h mp a t ht h r o u g ht h en o d e sa n dt h e d e f i n i t i o no fr e c o r d s ，a n dt h ee x c h a n g eo fl o c a lv a r i a b l e si nt h ep a t ho f c h a n g et ot h eo v e r a l lc h a n g ei nt h et r a n s f e r ，t h en u m b e ro fp a t h st o a c h i e v eo p t i m i z a t i o n p a p e r sa l s os t u d i e dt h ep r o b l eo ft h et r a n s f o r m a t i o n a n ds o r tb a s e do nt h ef a u l tt r e ea n a l y s i s ，ar a p i da n de f f e c t i v em e t h o do f l n p c p r o p o s e d ，t h e m e t h o d a d o p t e d t h e s t r a t e g y o f g r a d u a l d e c o m p o s i t i o no ft h e i n c i d e n t d i r e c t l y t o c o m p l e t et h e o r d e ra n d c o m b i n a t i o no fo n e t i m et oa c h i e v ef a u l tt r e et ot h et r a n s f o r m a t i o no f b d da n d o p t i m i z a t i o n ，a n dt h r o u g he x a m p l e s d e m o n s t r a t e i t s e f f e c t i v e n e s s o s m n p a l g o r i t h mu s i n gt h ee f f e c t i v ee x c h a n g eo fv a r i a b l e sa d j a c e n t p r o p e r t i e sa c c e s st oa tl e a s ts o r to fp a t h ；l n p ca l g o r i t h mb yt h er u l e s ，b y d e f i n i t i o n ，t r a v e r s i n gt h ef a u l tt r e ea tt h ee n do ft h ei n c i d e n tn o to n l y c o m p l e t e dt h eo p t i m i z a t i o ns o r t ，b u ta l s ot h ee f f e c t i v er e a l i z a t i o no ft h e f a u l tt r e et ot h et r a n s f o r m a t i o no fb d d ，t h e s er e s e a r c hr e s u l t so fb d d a p p l i c a t i o no f ab e t t e ri n d e p t ht h e o r e t i c a la n da p r a c t i c a lv a l u e t r e e k e yw o r d sb d d ，o b d d ，n o d e ，p a t h ，s o r to p t i m i z a t i o nf a u l t 原创性声明 本人声明，所呈交的学位论文是本人在导师指导下进行的研究 工作及取得的研究成果。尽我所知，除了论文中特别加以标注和致谢 的地方外，论文中不包含其他人已经发表或撰写过的研究成果，也不 包含为获得中南大学或其他单位的学位或证书而使用过的材料。与我 共同工作的同志对本研究所作的贡献均已在论文中作了明确的说明。 作者签名：卑 日期：丝年月竺日 学位论文版权使用授权书 本人了解中南大学有关保留、使用学位论文的规定，即：学校 有权保留学位论文并根据国家或湖南省有关部门规定送交学位论文， 允许学位论文被查阅和借阅；学校可以公布学位论文的全部或部分内 容，可以采用复印、缩印或其它手段保存学位论文。同时授权中国科 学技术信息研究所将本学位论文收录到中国学位论文全文数据库， 并通过网络向社会公众提供信息服务。 名：抖跏签名雄 硕士学位论文 第一章绪论 第一章绪论 1 9 9 4 年奔腾处理器的浮点运算错误和1 9 9 6 年阿里亚娜火箭的爆炸，再一次 向人们证实了保证系统设计正确性是至关重要的。但随着系统的复杂度的增大， 系统完备的置信工作受到验证技术限制。计算机科学在数据结构和高效算法设计 方面的一些研究成果有助于这个问题的解决。这个成果就是二元决策图( b d d ， b i n a r yd e c i s i o nd i a g r a m ) i ，它已经在许多c a d 项目和软件中得到了应用，并极 大地提高了设计性能。 1 1 研究背景 随着计算机软硬件系统日益复杂，保证系统的正确性和可靠性日显重要，为 此提出的许多理论和方法中，模型检测以其简洁明了和自动化程度高而引人注 目。 模型检验技术产生于8 0 年代初，由美国的c l a r k e 、e m e r s o n 法国的q u i e l l e 和s i f a l i s 分别独自提出。模型检验的基本原理是将原始设计表示成有限状态机， 将要验证的性质用事态逻辑来描述，然后遍历有限状态机以检验性质是否存在。 有限状态机通常采用k r i p k e 结构来描述，该结构在路径上是无限延伸的。模型 检验的优点是全自动的进行而无须人工机交互，当断定性质不满足时，模型提供 反例，以便于定位设计错误。但空间爆炸是模型检验的主要缺点，可以说模型检 验技术的发展历史就是不断寻找新思想、新策略、新算法来克服空间爆炸问题的 历史 1 9 8 6 年，b r y a n t 将传统的b d d 技术加以改进，使之成为布尔表达式的规范 表示o b d d ( 有序二元决策图，o r d e r e db i n a r yd e c i s i o nd i a g r a m ) 1 2 j 。m c m i l l a n 在1 9 8 7 年将这种技术应用于模型检验中，取得了巨大的成功。这种基于b d d 的 模型检验称为符号模型检验。 b d d 的引入使符号模型检验技术得到了飞速的发展。它本身也成为模型检 验工具的一个代表。 符号模型检验的主要思想是用b d d 来隐式地表示有限状态机的状态和状态 之间的迁移，其优点是能够表示一组而不是单个的状态和状态之间的迁移关系， 因此大幅度减小了空间需求。基于o b d d 的模型检验是以不动点理论为基础， 通过对不动点的计算隐式地实现了对状态空间的遍历，而不动点的计算是通过对 o b d d 实施标准化操作完成【3 l 。实验表明这种符号模型检验方法能处理的状态数 达1 0 2 0 量级，进一步改进的算法所能处理的状态数达到1 0 1 2 0 【4 1 。模型检测理论提 硕士学位论文 第一章绪论 出后，第一次在工业界取得了巨大成功，以前令验证人员感到棘手的复杂系统现 能够用这种工具自动验证。因此许多大型的i t 公司开始研究自己的模型检测工 具。实际上，符号模型检测在解决空间爆炸问题上迈出了一大步，但并没有彻底 解决空间状态爆炸这个难题。已使用的技术中存储和操作o b d d 时对内存要求 过大的矛盾随着设计系统的日益复杂更显突出。符号模型检测的研究虽取得了重 要的进步，但仍是一个充满了挑战的研究课题，国外的许多学者提出了很多新的 算法和改进算法，如偏序化简、组合推理、抽象、利用对称性、基于自动机的验 证等。 国内对这方面的研究起步较晚，开始于9 0 年代后期，主要集中于o b d d 的 在数字设计领域的应用，如逻辑验证【5 、综合【9 1 1 1 、自动测试生成( a t p g ， a u t o m a t i ct e s tp a t t e mg e n e r a t i o n ) 1 2 】等。同国外一样，模型检测技术首先的成功 在于硬件的检测，这是由于硬件电路本身的层次和规整性，较软件复杂的结构易 于描述和验证。随着理论研究的深入，现正在逐渐向人工智能【l3 1 、数字控制、系 统网络【1 4 1 7 1 等多方面渗透。 1 2 国内外研究现状 布尔代数是计算机科学和数字系统设计的基础，不同形式的布尔函数，只要 真值表相同，那么他们实质上是等价的逻辑函数。实际应用中，数字控制系统、 计算机辅助设计【1 8 1 、计算机辅助测试【1 9 1 、人工智能以及可编程控制器【2 0 】等领域 的许多问题都可以表示为一系列关于布尔函数的运算，这些运算有赖于布尔函数 的符号表示和算法的有效性，所以均可以用b d d 的方法进行研究 1 9 5 9 年l e e 提出来用b d d 来表示二元函数的数据结构，随后在这种基本模型 的基础上，a k e r s 做了很多不同方面的研究，从b d d 的结构构造到存储空间估算 【。1 9 8 6 年b r y a n t 指出，如果增加一些额外有序约束的a k e r s 模型可以有效的处理 二元函数l 引。因此提出了o r d e r e db i n a r yd e c i s i o nd i a g r a m 简称o b d d 。1 9 8 7 年， m c m i l l a n 在博士论文中，首次将o b d d 技术应用于模型检验中，从而大大地缓解 了空间爆炸问题。但o b d d 不是万能的，它的重要缺点是对于一些函数的表示仍 存在指数复杂度的问题。 1 9 9 0 年，b r a c e 、r u d e l l l 和b r y a i l t 基于有效i t e 的概念【引j ，提出了独立于变量 偏序的b d d 操作，它的主要算法是多根节点函数同时表示和i t e 的递归算法，共 享b d d 的提出，大大压缩t b d d 空间1 2 引。1 9 9 2 年，j a i n 等人在r o b d d 的基础上 引入了多个变量的索引，提出了i b d d ( i d e x e db d d ) 2 3 1 ，从而扩展了r o b d d 的表示范围。i b d d 的特点是节点的分层，每一层节点以r o b d d 的形式表示，不 同的层可有不同变量编序方法。i b d d 的表达式是多项式的复杂度。1 9 9 3 年，l a i 2 硕士学位论文 第一章绪论 等人则提出了一种层次结构描述的边值e v b d d ( e d g e v a l u e b d d ) 【2 4 j ，e v b d d 可在高级的功能级上来描述变量的编序，并为层次化的功能验证、测试提供有 效的工具。 在其后发展过程中，出现了一些基于r o b d d 的扩展结构，如b a l l a ：的a d d ( a l g e b r a i cd e c i s i o nd i a g r a m s ) 【2 5 】和m i n a t o 的z d d ( z e r o s u p p r e s s e db d d ) 【2 6 1 ，都在 相应领域取得好的效果。a n d e r s e n 于1 9 9 7 年提出b e d ( b o o l e a ne x p r e s s i o n d i a g r a m s ) 口7 】的结构，它以r o b d d 为基础，将布尔算符作为节点在图中表示。 1 9 9 8 年，g u n t h e r 和d r e c h s l e r 又提出线性变换的算法，它不是变换整个b d d ， 而只是把输入变量进行线性变化。对于许多系统来说都能大大减少他们的图的规 模和运行时间1 2 8 - - 3 0 1 。但对于有些系统，这种方法找不到一个合理的变换，甚至 回增加他们的b d d 的节点数。 上述的研究都在不同程度上简化了节点，减少了运行时间，但是随着系统规 模的不断增大，b d d 表示与操作的复杂性仍很高。 国内对b d d 的研究比较晚，主要集中在b d d 的应用：集成电路领域的逻辑 综合及电路等价性验证，安全结构体系中故障树分析【3 l 】、网络系统中可靠性研究 【1 4 】【3 2 】等，都取得了较好的成效。根据其数据结构及良好的操作性能，人们逐渐 把b d d 的这种工具也运用到图论【3 3 】、人工智能搜索【3 4 1 、网络流量【1 3 1 的计算、安 全库规则的配置【3 5 l 3 6 1 1 等多项领域。近段，人们已开始着手研究b d d 在知识表达 和推理领域【3 7 】，知识模型检测【3 8 】【3 9 1 及安全协谢3 6 1 验证等领域的应用探索。 在b d d 的发展研究中表明b d d 的算法运行时间与b d d 的规模数量成多项式 的关系，而b d d 的规模敏感依赖输入变量的顺序。因此，b d d 的变量排序优化 算法成为了b d d 领域的研究热点。目前在b d d 优化算法中主要有精确排序算法1 4 0 1 和动态启发式算法【4 1 1 1 4 2 1 两类。但改进b d d 的变量排序本身就是一个n p 问题f 4 3 j 。 目前人们正在寻找其他的解决办法。 一方面根据应用目标需要对传统的方法( 精确排序【4 0 】和动态重排序【4 1 1 ) 进 行改良和优化】【4 5 】；精确排序实质上一种隐式枚举法，虽然有严格的数学理论 为基础，但算法的时间复杂度为d ( 3 ”刀2 ) ，只适合变量很小的函数。动态重排 序利用相邻变量排序交换只影响交换两层节点的思想，它的优点在于对一个n p 问题给出了一个多项式时间的算法，不存在计算机能否实现的问题，在排序优化 中成为了研究的核心。但其弱点是它提供的非真正意义上的最优解。在经典优化 的算法中，动态算法依然有较大的发展空间，如何将遗传算法、模拟退火算法等 一些传统的启发式引入，完成对动态算法的改进和优化，是一个值得关注的研究 方向。 另一方面根据实际的应用引入启发式策略来确定优化目标：如在以往的应用 硕士学位论文 第一章绪论 研究中主要关注b d d 节点的规模，因此b d d 的规模优化就变成了节点的优化， 随着应用的深入和广泛，一些应用中对节点的关注可能转化为b d d 的其他目标。 近几年，国外的研究者已开始重视这些方面的研究，并做了大量的工作。比如对 路径的关注在实际运用中已日显突出。电路的测试中，由于电路的路径直接对应 于b d d 中的路径】，最小化路径数量可以大大减少测试矢量生成，减少测试时间 9 】：同样由于函数的赋值时间对应着b d d 平均路径( e p l ，e x p e c t e dp a t h l e n g t h ) ，逻辑电路中，不同输入变量出现的概率是不相同的，不同的输入组合 对应的符值时间也不相同，所以拥有最小的e p l 的b d d 将得到最小的符值时间 【5 0 1 。当然还有电路中信号的延时【5 、空间问题求解搜索都关联着b d d 的路径。 b d d 的最少路径、最长路径和平均路径都因其在数字电路中的实际意义而备受关 注。 1 3 研究内容 国内外研究现状表明，b d d 的结构规模敏感的依赖变量排序，b d d 操作时 间与b d d 规模成多项式关系。如何找到一个最优的排序来得到最优化的结构依 然是b d d 研究的关键点。本文将路径数量的最小化作为b d d 路径优化的目的， 针对路径数量最小化的变量排序优化进行了做了分析研究，提出了路径数量最小 化的变量排序算法o s m n p ( t h eo p t i m i z e ds o r tw i t hm i n i n i z en u m b e rp a t h ) ，并验 证证实了它的有效性；同时对节点优化给出了改进的思路。 b d d 是故障树分析的最有效工具之一，但由于底事件的排序严重影响着 b d d 的结构，使故障树的定型和定量分析中依然存在着组合爆炸的问题口。本文 针对排序和转化的方法做了研究，提出一种逻辑相邻优先组合( l n p c ，l o g i c n e i g h b o rp r i o r yc o n n e c t i o n ) 方法来实现故障树向b d d 的转化。该方法将门事件 和底事件视为同一性质事件，一同参与排序和组合；通过从上至下遍历故障树逐 步获取底事件的排序，遍历时既考虑了子事件位置上的关联，也考虑了子事件逻 辑上的相邻；同一门下的子事件排序完成后进行组合化简，这样边排序、边组合 化简直接得到了节点规模最优化的b d d ；并通过故障树的实例证实了该算法的 有效实用。 1 4 论文组织结构 论文全文共五章，论文的各章节组织安排如下： 第一章为绪论。介绍课题的研究背景和意义，着重对国内外基于b d d 技术 理论和应用研究现状进行了论述和分析，最后指出论文的研究内容和组织结构安 排。 4 硕士学位论文 第一章绪论 第二章介绍了b d d 的相关基础理论。重点介绍几种常用b d d 的结构及操 作算法；分析了几种b d d 优化结构。 第三章研究了利用变量排序来优化b d d 路径的方法。首先阐述了变量序对 b d d 节点数量的影响，对节点规模的排序优化算法做了分析，给出了筛选算法 的改进思路；然后对b d d 路径数量的排序优化做了深入地研究，指出路径中传 递链存在是路径优化的关键，依此对b d d 中路径数量的记录与传递研究了相应 了策略，提出了路径数量优化的o s m n p 算法，并验证了该算法的有效性。 第四章研究了基于b d d 的故障树分析的转化方法和排序问题。首先对常用 的两种转化方法和排序的方法进行了分析，在此基础上提出了一种快速有效的 l n p c 方法完成故障树到b d d 的转化和优化。l n p c 方法通过遍历故障树而直 接得到其节点优化的b d d 。b d d 没有采用固定的变量排序；不需要先写出故障 树的布尔函数；同时边排序边组合边化简有效的减少了b d d 的存储空间，使b d d 一直以紧密的结构存储在计算机中，减少了内存空间的复杂度。最后通过实例对 算法进行了详尽的描述，验证了其有效性。 第五章对全文的研究工作进行了总结，指出了论文的不足，并对进一步的工 作进行了展望。 硕士学位论文第二章二元决策图的基本原理 第二章二元决策图的基本原理 a k e r s 最早提出用b d d 来描述布尔函数f l 】b r y a n t 对b d d 施加了些约束从 而使b d d 成为布儿函数的正则表示方法【2 1 。与其它的表示方法相比，b d d 的优 点是表达紧凑，易于操作，现已成功的运用于使用于模拟、验证【5 2 1 、判定3 9 1 等 问题的求解。 2 1 二元决策图的基本概念 b d d 是基于s h a n n o n 的布尔函数展开理论，在函数逐层展开过程中对各个变 量进行0 或l 的赋值，体现在图中就是相应的节点及其0 和l 的两个后继分支， 直到函数的终值。b d d 的出现，使传统的对布尔函数的分析可以转化为一系列 图的运算、约束、遍历等操作，从而为更高效的应用提供了可能。 1 二元决策图的定义 二元决策图是布尔函数的一种图的表现形式，因为这种图中的变量的取值只 有0 和l ，所以称之为二元决策图即b d d 。相对布尔函数的其他描述方法，b d d 来表示布尔函数所用的存储空间较少，可以极大的提高模型检验的系统规模。 定义2 1 二元决策图是一个具有有限个节点的有向无环图，g = 。其 中v 是g 中所有节点的集合，e 是所有边的集合【】j 。 b d d 的节点包含终节点和非终节点。终节点没有输出边，且只能用o 和l 两个值表示，每个非终节点用一个输入变量表示，且有两条1 和0 的输出边，l 表示这个节点变量取1 时的分支，0 表示这个节点变量取o 时的分支，每个b d d 有且只有一个根节点。 在表示b d d 时，通常规定所有的非终节点都由一个含有变量的圆圈表示， 而所有的终节点都由含有一个0 或1 的值的方框来表示。所有的“0 ”边都用虚 直线来表示，所有的“1 ”边都由实线表示。 布尔函数厂= x i x 2 x 3 + x 1x 2 x 3 + x i x 2 x 3 ，它的b d d 如图2 1 所示。 图2 - 1f 的b d d 6 硕士学位论文 第二章二元决策图的基本原理 2 二元决策图的构造 用函数= x i x 2 x 3 + x i x 2 屯+ 一x 2 石3 来说明如何得到一个布尔函数的b d d 。 ( 1 ) 每一个布尔函数：厂：b ”专b 都可以用香农定理在每个一个节点上展 开，最终构成一个有向无环图。 定理2 1 一个n 个变量的布尔函数f ( x 。，x ：，j 。) ( o ，1 ) 在变量t 处可以表示 为： f = 一卅t = 0 + x i f i x , = 1 公式( 2 - 1 ) 公式2 1 称为香农定理。上式为函数厂在变量x 。处的展开，把变量x ，称为函 数厂的分解变量，卅x 。= 0 为关于毛的负因子，厂i 一= 1 为关于_ ) c ，的正因子。布尔 公式的递归香农展开对应着一个递归的二叉判定树。见图2 1 中可以看出，对于 一棵二叉判定树，根结点对应于原函数，它的左孩子表示函数f i x , = 0 ，右孩子 表示函数1 i x 。= l 。 ( 2 ) 确定一个变量排序，而 x 2 毛 x 4 。 “ 这里表示“排序在前面”。x i 为第一个排序变量，也就是根节点，它有 两个取值分支1 分支和0 分支，1 分支用实线标识，o 分支用虚线标识，分别指 向对应最1 1 = x 2 x 3 + x 2 x 3 - - - - x 3 ，f ；【l 可= x 2 x 3 函数，这两个节点用这个函数中排序最 前的变量标识。继续按变量序对这两个函数分别使用香农定理，依次得到相应的 节点。完整的b d d 如图2 1 。 其中基于任何一个函数的b d d 不是唯一的，不同的变量排序得到的b d d 是不相同的。 。 3 有序的二元决策图 定义2 2 有序的二元决策图是在b d d 的基础上对函数的变量进行排序产 生的b d d ，即选定了变量的先后顺序的b d d ，简称o b d d ( o r d e r e db b d ) 【1 】。 设o b d d 的节点集合为，o b d d 的每个非终端节点y 有一个索引值，即 i n d e x ( v ) 1 ，2 ，甩 ，节点，还有两个孩子节点l o w ( v ) ，h i g h ( v ) v 。 如果l o w ( v ) 也是非终端节点，则i n d e x ( v ) i n d e x ( 1 0 w ( v ) ) ，同理若m g h ( v ) 也 是非终端节点，则i n d e x ( v ) i n d e x ( h i g h ( v ) ) 由定义可知，当沿o b d d 的根节点向下搜索时，每个节点在每条分支上出现 的次数最多一次且变量出现的顺序相同。根节点的索引值为1 ，终节点的索引值 为n + l 。 4 二元决策图同构 定义2 3 两个o b d d 图g 和g 是同构的，当它们存在一个从g 到g 7 的节点 一一对应的函数s ，对于任意一个节点v ，如果s ( v ) = 1 ，则节点v 和v 有 i n d e x ( v ) = i n d e x ( v ) ，s ( 1 0 w ( v ) ) = l o w ( v , ) ，s ( h i g h ( v ) ) = h i g h ( v ) 7 硕士学位论文第二章二元决策图的基本原理 由于每个函数图只有一个根节点并且它的任意非终端节点的孩子都是不相 同的，因此要求g 和g 之间的同构映射严格遵循图g 的根节点对应图g 根节 点，图g 的根节点的o 边对应图g 的根节点0 边，图g 的根节点的1 边对应g 的l 边，这样一一对应相等，直到终端节点。这样很容易检查两个o b d d 是否 同构。 若两个o b d d ，g 和g 7 是同构的，那么它们对应节点的子图也是同构。 5 简约的二元决策图 定义2 5 当一个有序二元决策图中不包含同构子图且节点的两条分支不指 向同一个节点时，称这个有序二元决策图为简约的有序二元决策图，即r o b d d ( r e d u c e da n do r d e r e db d d ) 。 一个o b d d 可以通过以下三条规则转化为r o b d d ，设o b d d 为g = 1 ) 合并终节点中相同的节点，使之最多只有两个终节点，且它们的取值只 可能为0 或1 。 2 ) 对非终节点u 和v ，如果v a r ( u ) = v a r ( v ) ，l o w ( u ) = l o w ( v ) ，h i g h ( u ) = h i g h ( v ) 这三个式子成立，则删除其中一个节点，将删除节点的所有入边指向保留节点。 3 ) 对于非终结点v ，如果有l o w ( v ) = h i g h ( v ) ，则删除节点v ，并将它的所有 入边指向l o w ( v ) 。 一般来说，这三条规则要反复使用，因为每次应用其中一条规则进行化简产 生新的o b d d 都可能需要应用其他两条进行进一步化简。b r y a n t 提出一个称为 r e d u c e d 的过程，该过程能够以自上而下的方式在线性时间内完成化简过程。 2 2 二元决策图的基本操作 常用的对b d d 的操作有多种，这里主要介绍化简( r e d u c t ) ，通用( a p p l y ) 和i t e ( i t e t h e n e l s e ) 运算。 1 o b d d 数据结构 b d d 是布尔函数的图形表示，建立在两个布尔函数上的运算同样可以通过 它们的o b d d 的操作来完成。首先要完成对o b d d 的节点建模，b d d 中的非终 节点有两条分别为0 、l 的输出边，采用下面的基本数据结构来描述： 8 硕士学位论文第二章二元决策图的基本原理 s t r u c tn o d e i n ti n d e x ； i n t i d ； b o o l e a nm a r k ； v a l u e ( 0 ，1 ，x ) ； n o d eh i g h ； n o d el o w ； ) 胪变量的索引； 木变量标记； 胪变量标志； 胪表示函数值，是枚举类型( e n u m ) ； * 1 输出边对应的节点； h * o 输出边对应的节点； b d d 的运算操作是建立在b d d 的图的表示之上的，当然在实际运用中我们 可以对它的数据结构做相应的修改。 2 简化算法 简化算法可以把一个函数的b d d 简约为r o b d d ，它是利用检验两个图是 否同构来达到简约的目的。用v 来表示节点，节点的标识用一个整数i d 来唯一 标识它i d ( v ) 。i n d e x ( v ) 表示这个节点所对应变量的索引，i d ( 1 0 w ( v ) ) 表示这个节点 的1 输出边对应的节点，i d ( h i g h ( v ) 1 表示这个节点的0 输出边对应节点。根据前 面所谈到的b d d 向o b d d 转化的规则，可以表示成下面两条，( 1 ) i n d e x ( u ) = i n d e x ( v ) ，i d ( h i g h ( u ) ) = i d ( h i g h ( v ) ) ，i d ( 1 0 w ( u ) ) = i d ( 1 0 w ( v ) ) ；此两节点同 构，删除其中一个；( 2 ) i d ( h i g h ( u ) ) = i d ( 1 0 w ( u ) ) 表明此节点的0 、1 输出指向同 一节点，此节点为多余，删除此节点，并将指向此节点的输入指向i d ( 1 0 w ( u ) ) 。 此算法的复杂度由节点来决定，如果g 由m 个节点构成，则其最大的时间 复杂度o ( m l o g m ) 3 通用算法 在o b d d 上定义通用的逻辑运算，如与、或、非等。通用逻辑运算包括1 6 种二元运算。b r y a n t 提出一个称为a p p l y 的过程来统一处理1 6 种逻辑。提供了 两个代表布尔函数f 1 和f 2 的o b d d ，通过一个o p 操作来得到一个代表两个 函数f 1 f 2 结果的o b d d 。 阢 六j ( x l ，x 2 ，。，x 。) = z ( x l ，x 2 ，。，x 。) ( x l ，x 2 ，矗) 是操作符，可以是a n d 或o r 异或等1 6 种运算。 此算法由函数的根节点向终节点由上而下进行，在结果图上产生一个由两个 图的节点合成的节点。算法的主要依据是递归运用香农定理： 石 = t ( z i x ，= 0 厶k = 0 ) + x ( z i x f = 1 i x ，= 1 ) o 硕士学位论文 第二章二元决策图的基本原理 对这个算法需要考虑的有以下几点： 若两个节点为终节点，则得到的合并图由终节点组成，且终结点的值为两 节点 得到； 若两个节点为非终节点，且变量序相同，则直接将对应输出 操作， 得到新的合并点； 且两节点的变量序不同，则需要将小变量序的0 1 输出均与变量序高的节点 操作，得到新的合并节点。下面用伪代码写出其算法。 a p p l y ( o p ，”2 ) i fu l 0 ，l a n du 2 o ，1 ) u 卜o p ( u l ，u 2 ) ) e l s ei f i n d e x ( u 1 ) = i n d e x ( u 2 ) u 卜i n d e x ( u 1 ) ，a p p l y ( 1 0 w ( u 1 ) ，l o w ( u 2 ) ) ，a p p l y ( h i g h ( u 1 ) ，h i g h ( u a ) ) ) e l s ei fi n d e x ( u 1 ) i n d e x ( u 2 ) u 卜i n d e x ( u 2 ) ，a p p l y ( u l ，l o w ( u 2 ) ) ，a p p l y ( u 1 ，h f g h ( u 2 ) ) ) r e t u r nu ) 下面用图来描述：厂= 厂laf 2 ，变量序列为x 1 x 2 x 3 h i g h ，h v - h i g h ) ； e = i t e ( f v - l o w ，g v - l o w ，h v - l o w ) ； i f ( t = e ) r e t u r nt ： b d d _ i n s e r t ( v ，t ，e ) ； ) 胪得到下一个待分解的原始输入量 胪对节点v 的l 边递归调用i t e 算法 幸对节点v 的0 边递归调用i t e 算法 铲撬入节愚 用图2 3 描述此算法：图2 3 中函数鲰l + x 2 ，g = x l x 3 ，h = x 2 x 4 ，所对应i 钓b d d 分别为f ，g ，h ，i = i t e ( f ，g ，h ) 。 图2 - 3i = i t e ( f ，g ，a ) 的计算 2 3 二元决策图结构优化与扩展 1 2 硕士学位论文第二章二元决策图的基本原理 为了优化b d d 的存储结构，减少操作的复杂度，引入了补边( c o m p l e m e n t e d e d g e s ) 5 3 1 和共享二元决策图( s b d d ，s h a r e db d d ) p 2 的概念。 1 补边 很多o b d d 中，函数和函数的反函数同时出现，为了减少o b d d 的节点，引 入补边( c o m p l e m e n t e de d g e s ) 来表示反函数。这种技术的依据只因为函数饼其厂 的o b d d 结构只有一点不同，就是其终节点的值相互交换。给o b d d 中节点的边 设置一个补边位属性，若边没有设置补边属性，则其指向的函数就是原函数体 身，若设置了，它指向函数的反函数厂。这样函数厂和厂只用一个点即可表示。 在采用用补边的o b d d 中，终节点只用l 即可，o 为可以用l 的取反表示。 图2 4 中函数厂= 而+ 秘一f ：五面 ( a ) 没有引入补边f 和f 的b d d( b ) 引入补边的f 和f 的b d d 图2 - 4 有补边和无补边的b d d 引入补边后，也将面临一个这样的问题，函数的b d d 表示失去了其规正形 式。为此约定，补边只设置在0 边上。一个带有两个输出，一个输入的节点x i ， 它有8 个可能的方式来设置其补边。根据得摩根定律：下面的这些成对出现的方 式在功能上是等效图： 一 图2 - 5 函数的成对等价表示 专 硕士学位论文第二章二元决策图的基本原理 为了得到b d d 形式规整化，建议用左边的形式来取代右边的形式。 补边的使用使o b d d 的性能在下面几方面得到了改善： 1 ) o b d d 的结构更加紧密，使用补边，o b d d 的大小可以减少到7 2 ) 简化了函数的求反操作，使其在一个常数时间内完成操作。 3 ) 补边的引入可以使布尔操作中更方便的使用这些规则：厂+ f = l ， f = 0 2 共享二元决策图 如图2 6 所示，几个函数可以用一个带有多个输出的有向图来表示，这样出 现在几个o b d d 中的子图只需表示一次即可。这种技术技术称之为共享二元决策 图即s b d d 。 图2 - 6 函数f 1 ，f 2 ，f 3 共享0 b d d 共享o b d d 大大节约了时间和空间。同样也简化了部分操作，比如两个函数 的比较，可以转化为对它们的根节点比较。 3 自由排序二元决策图 自由排序二元决策图( f b d d ，f r e eb i n a r yd e c i s i o nd i a 黟a m s ) 是针对受了约 束的o b d d 而言，实质上是一种非固定排序的b d d ，但在任一分支上每个变量 只出现一次1 5 4 1 。o b d d 并非一种完善的图的结构，它的缺陷主要是b d d 对排序 的敏感；特别是b d d 采用统一的固定排序，这种约束在一些情况约束了b d d 最优结构的产生。比如整个b d d 表示的函数是由多个不相关联的系统组成时， 不同的子系统采用不同的排序时，得到的规模更小。f b d d 虽然在全局的b d d 中并不存在一个固定的排序，但在一条路径上，它的每个变量只出现一次；它采 用了类似o b d d 化简规则，也同样保留了类似o b d d 的许多好的属性：精简性、 唯一性等。所以在不相关的多子系统中，采用它来获得最优化的结构几率要大， 但又保留了所需要的属性。第四章采用了这种非固定排序的方法来获得节点优化 的b d d ，同时保留得到的割集。 函数f = 五x 2 x 3 + x x 2 x 4 + x l 屯_ + z l z 2 x 3 ，图2 - 7 ( a ) 对应函数f 的f b d d ， 图2 7 伯) 对应函数f 的o b d d 1 4 硕士学位论文 第二章二元决策图的基本原理 ( a ) f 的f b d d 2 5 本章总结 图2 7f 的0 b d d 和f b d d ( b ) f 的o b d d 本章介绍了b d d 、o b d d 、r o b d d 的基本概念对o b d d 中常用的基本操 作算法做了说明，列举优化b d d 结构的的几种措施，对b d d 扩展家族成员的 f b d d 做了相关的说明。 硕士学位论文 第三章二元决策图的排序优化 第三章二元决策图的排序优化 o b d d 作为布尔函数的一种图的描述和其他有向无环图一样，它的结构包含 两类信息：节点v 和边e 。用计算机来实现对o b d d 操作首先要考虑它的存储。 计算机存储o b d d 节点的信息，边的信息隐含在节点和节点的关联中。由于 o b d d 规模结构对应着计算机实现算法的空间和时间复杂度，所以往往o b d d 的规模用节点的数量来衡量；随着o b d d 理论研究的深入和o b d d 应用的广泛， 路径也逐渐成为研究的另一个关注点。研究表明路径与节点的数量都敏感的依赖 变量的排序，如何取得一个最好的排序来得到最优化的结构一直是研究的热点。 3 1b d d 结构与排序 研究表明b d d 结构中的两类信息节点和路径数量都依赖变量的排序。 1 节点与变量序 一个b d d 的节点规模敏感的依赖于其构造所选择的变量顺序。从理论上分 析一个含有n 个变量的布尔函数其对应的b d d 的节点数范围是【n + 2 ，2 n + l 】，也 就是在最好情况下一个变量只生成一个节点最差情况下节点数随着变量个数的 增多呈指数级增加。 函数f = x i x 2 + x 3 毛，若它的变量序分别为l = ( x i , x 2 ，x 3 ，x 4 ) 和2 = ( x l ，x 3 ，x 2 ，x 4 ) ，产生的o b d d 分别由图3 1 ( a ) ，图3 - 1 ( b ) 给出。 ( a ) 变量序丌1 下的b d d ( b ) 变量序丌2 下的b o o 图3 - 1f 在变量序丌- 7 rz 下的b d d 图3 1 ( a ) 中o b d d 有4 个非终节点而在3 1 ( b ) 中b d d 有6 个非终节点。 对大规模的电路其影响会更大因此寻找一个好的变量排序是非常重要且必须。 2 、路径与变量序 b d d 的节点数量敏感地依赖变量序，事实上变量排序同样影响b d d 路径数 1 6 硕士学位论文第三章二元决策图的排序优化 量