（计算机软件与理论专业论文）bddrpa：基于obdd的rpa算法.pdf

b d d r p a * ：基于o b d d 的r p a 算法 b d d r p a * ：基于0 b d d 的r p a * 算法 专业：计算机软件与理论 硕士生：徐艳艳 指导老师：苏开乐 摘要 在人工智能领域，不确定的动态环境下的重搜索问题的求解空间、时间复杂 度都是比较大的，如何改进算法以提高重搜索效率就成为研究者们一直关注的问 题。在一般的搜索问题中，随着搜索深度的增加，状态空间也是呈指数爆炸的， 经典的避免状态数目爆炸的方法是使用启发方法( a + 算法) 来引导搜索路径至 目标节点。最近的几年中，在模型检测领域上基于o b d d 的搜索技术得到较快的 发展，这种技术可以使得搜索的状态空间达到1 0 ”o 【7 ，8 。在近两年研究成果基 础上，本文对如何把启发方法( a 算法) 、基于o b d d 的搜索技术和渐进搜索 ( i n c r e m e n t a ls e a r c h ) 结合在一起，从而改进重搜索算法这一问题进行了研究。 本文提出了一个在动态环境下的搜索算法b d d r p a * ，它的优点是可以应用 到动态的持续变化的领域中，例如持续规划问题、移动的机器人问题等。这些问 题的特点是系统的状态随时间不断发生改变，因此，初始的规划会变得不太合适 甚至不能再使用。一般的处理方法是对新的状态的全局进行重新搜索，从而得到 新的规划来执行。但是，我们发现在较多的问题中，这些改变是局部的，对于整 个系统来说都往往是比较小的。这样，由于搜索状态的改变只是一小部分，那么 再进行一次彻底的搜索就显得不必要，因为我们可以利用上很多原先的搜索记 录，这样可以减少我们的搜索空间和时间，这就是渐进搜索的基本思想。而 b d d r p a * 算法就是综合了渐进搜索和基于o b d d 的启发式搜索方法而提出的。 本文首先简要地介绍了经典的搜索算法( 比如a ，宽度优先搜索算法等) ， 和基于o b d d 的搜索算法b d d a * 和s e t a * ；接着详细介绍了我们提出的 p r e - b d d r p a * 算法以及在它基础上做了改进后的正式的b d d r p a * 算法，我们给 出了该算法的c + + 伪代码并对其做了一些详细的分析；然后通过实验将 b d d r p a * 和b d d a * 算法、l p a * 算法、a 算法以及b f s 宽度优先等重搜索算法 b d d r p a * ：基ro b d d 的r p a * 算法 进行比较，实验结果证明，b d d r p a * 算法确实能提高了重搜索的效率：最后， 我们探讨了b d d r p ”在自动规划、机器学习和自动控制三个领域上的应用前景。 关键词：人工智能，模型检测，二叉决策图，渐进搜索，a ，算法 i i b d d r p a * ：基于o b d d 的r p a * 算法 b d d r p a 去：a no b d d - b a s e d r e p l a n n i n g h e u r i s t i c s e a r c ha l g o r i t h m m a j o r ：c o m p u t e rs o f t w a r ea n dt h e o r y n a m e ：y a n y a nx u s u p e r v i s o r ：k a i l es u a b s t r a c t i nt h i sp a p e rw es t u d yt h es e a r c h a l g o r i t h m sb a s e do no b d di n a r t i f i c i a l i n t e l l i g e n c e a r e a i ti s a l w a y sd i f f i c u l t t os o l v e p l a n n i n g p r o b l e m si na ia r e a t i m ec o m p l e x i t ya n ds p a c ec o m p l e x i t yo ft h e s e p r o b l e m sa r en p c o m p l e t ea n dn p s p a c er e s p e c t i v e l y s oi ti si m p o r t a n t f o ru st od e s i g ns o m eb e t t e rs e a r c ha l g o r i t h m si no r d e rt oi m p r o v et h e s e a r c he f f i c i e n c y d u r i n gt h el a s td e c a d e ，p o w e r f u ls e a r c ht e c h n i q u e su s i n ga l li m p l i c i t s t a t er e p r e s e n t a t i o nb a s e do nt h er e d u c e do r d e r e db i n a r yd e c i s i o nd i a g r a m h a v eb e e nd e v e l o p e di nt h ea r e ao fs y m b o l i cm o d e lc h e c k i n g s i m i l a r r e s u l t sh a v e b e e no b t a i n e di n w e l l s t r u c t u r e da is e a r c hd o m a i n s h o w e v e rf o rh a r dc o m b i n a t o r i a lp r o b l e m st h es e a r c hf r i n g eo f t e ng r o w s e x p o n e n t i a l l yw i t ht h es e a r c hd e p t h ac l a s s i c a la ia p p r o a c hf o ra v o i d i n g t h es t a t ee x p l o s i o np r o b l e mi st ou s eh e u r i s t i c st og u i d et h es e a r c ht o w a r d t h eg o a ls t a t e s s ow h e t h e rh e u r i s t i c sc a nb ea p p l i e dt oo b d d b a s e d s e a r c hs u c ht h a tt h e i ra b i l i t yt oe f f i c i e n t l ye x p a n da l a r g es e to fs t a t e si n t t t b d d r p a ，：基于o b d d 的r p a * 算法 e a c hi t e r a t i o ni sp r e s e r v e d i nt h i sp a p e r , w ep r e s e n tan e ws e a r c ha l g o r i t h mc a l l e db d d r p a + t h em a i ni d e ao fi t i st oi m p r o v es e a r c he f f i c i e n c yb yc o m b i n i n gt h e i n c r e m e n t a lh e u r i s t i cs e a r c ht e c h n i q u ea n do b d d a sw ek n o w , s e a r c h a l g o r i t h m sb a s e do no b d d c o u l di m p r o v es e a r c he f f i c i e n c y o u rp a p e ri s o r g a n i z e da sf o l l o w s f i r s tw eb r i e f l yd e s c r i b ea 8 o b d d sa n db d d b a s e ds e a r c h t e c h n i q u e s w e t h e nd e f i n et h e b d d r p a + a l g o r i t h ma n de v a l u a t ei te x p e r i m e n t a l l yi nar a n g eo fs e a r c h a n d p l a n n i n gd o m a i n s f i n a l l yw ed r a wc o n c l u s i o n sa n dd i s c u s s d i r e c t i o n sf o rf u t u r ew o r k k e yw o r d s ：a r t i f i c i a li n t e l l i g e n c e ，m o d e lc h e c k i n g ，o b d d ，i n c r e m e n t a l s e a r c h ，a + a l g o r i t h m b d d r p a * ：基一f - o b d d 的r p a 算法 引言 一直以来，在人工智能领域，智能规划的求解是困难的，规划问题的空间、 时间复杂性都是n p 完全的：因此，如何改进算法以提高搜索效率就成为一个至 关重要的问题。 现在，通过搜索时间和结果路径的代价交替换位，已经逐步发展了儿种加 速搜索的方法。这里面包括使用不可采纳的启发搜索( i n a d m i s s i b l e h e u r i s t i c s ) 1 ，2 和带1 i m i t e dl o o k a h e a d 的搜索 3 ，4 ，5 ，后者也叫 r e a l t i m e 或a g e n t c e n t e r e d 搜索。而在我的论文里，我将关心一种特别的加 快搜索的方法：i n c r e m e n t a ls e a r c h i n c r e m e n t a ls e a r c h 是一个为c o n t i n u a l p l a n n i n g ( 也可以称之为r e p l a n n i n g ，p l a nr e u s e 或1 i f e l o n gp l a n n i n g ) 而 发展的搜索技术 6 。这种技术重复使用以前的搜索得到的信息去找到一系列相 似的搜索问题的解。我们认为，这种搜索技术比从头开始解决每个搜索问题快。 与其它一些的加快搜索的技术不同的是，它能保证找到最短的路径解，也就是说， 它是可采纳的。 另一方面，在过去的十年中，基于o b d d 的强大的搜索技术在符号化模型 检测领域发展起来了，使用这种技术可以成功检测至1 0 n 1 3 0 的状态空间 7 ，8 。 在舡的搜索问题中，随着搜索深度的增加，状态空间也是呈指数爆炸的 9 】。因 此，如何把r p a * 算法和基于o b d d 的搜索技术结合在一起以改进搜索算法就很 值得研究了。 在近几年，各种各样的基于o b d d 的搜索技术以改进搜索算法的成果不断涌 现，其中最出名的是b d d a * 算法 1 0 和s e t a * 算法 1 1 。尽管它们在某种程度上取 得了成功，然而，正如我们知道的那样，每个算法都有其局限性和不足，所以对 于算法的设计和改进是无止境的。 在本文中，我们提出了一个新的搜索算法b d d 雎a + 。正如前面所提到的， 像l i f e l o n g a 4 算法一样，它可以被应用到动态的持续变化的规划领域中，比如持 b d d r p a * ：基于o b d d 的r p a * 算法 续规划问题、移动的机器人问题等。这些问题的特点是系统的状态随时间不断发 生改变，因此，初始的规划会变得不太合适甚至不能再使用，我们不得不对新的 情景重新规划。幸运的是，这种改变相对于整个状态系统来说往往是比较小的。 这样，由于搜索问题的改变只是一小部分，所以，先前的搜索结果很多可以重新 被使用，那么，再进行一次彻底的搜索就显得不必要。b d d r p a * 算法的思想就 是把o b d d 的搜索技术和渐进搜索( i n c r e m e n t a ls e a r c h ) 6 】以及启发式( a + 算法) 方法结合起来。 本文的结构如下：第1 章我们对人工智能领域的搜索算法 1 2 ，1 3 ，1 4 1 以及 o b d d 1 5 ，1 6 做了一些简单的介绍；第2 章我们介绍了两个比较出名的基于 o b d d 的搜索算法b d d a + 1 0 】和s e t a * 1 1 】，这也是目前仅有的基于o b d d 的启 发式搜索算法，这有利于对b d d r p a * 的理解以及后面实验的分析比较；第3 章 我们提出了l o r e b d d r p a + 算法以及在它基础上做了改进后的正式的b d d r p a * 算法并对它进行了详细的分析；第4 章通过做实验我们把b d d r p a * 和b d d a * ， l i f el o n ga + ( l p a + ) 【6 】，a + 以及b f s 进行了分析比较；第5 章对b d d r p a * 的应 用领域做了一些介绍；第6 章我们总结全文并简单说明了下一步要做的工作。 b d d r p a * ：基jo b d d 的r p a + 算法 第1 章人工智能领域的搜索算法肺以及o b d d 的介绍 人工智能( a r t m c i a li n t e l l i g e n c e 或简称址) 有时也称作机器智能，是指由人制 造出来的系统所表现出来的智能。通常人工智能是指通过普通计算机实现的智 能。 人工智能包括一些不同的研究领域，比如自然语言处理、自动定理证明、智 能数据检索系统、机器学习、模式识别、视觉系统、问题求解、人工智能方法和 程序语言以及自动程序证明等。 其中，在问题求解( p r o b l e ms o l v i n g ) 领域，人工智能的第一大成就是发展 了能够求解难题的下棋( 如国际象棋) 程序。在下棋程序中应用的某些技术，如 向前看几步，并把困难的问题分成一些比较容易的子问题，发展成为搜索和问题 规约这样的人工智能基本技术。到目前为止，人工智能程序已知如何考虑要解决 的问题，即搜索解答空间，寻找较优的解答。问题求解是个大课题，它涉及规约、 推断、决策、规划、常识推理、定理证明和相关过程的核心概念。在分析了人工 智能研究中运用的问题求解方法之后，就会发现许多问题求解方法是采用试探搜 索的方法。也就是说，这些方法是通过在某个可能的解空间内寻找一个解来求解 问题的。 1 1 图搜索策略 每种以知识和符号操作为基础的智能系统，其问题求解方法都需要某种对解 答的搜索。不过，在搜索过程开始之前，必须先用某种方法或某几种方法的混合 来表示问题。对于同一问题可以有多种不同的表示方法，这些表示具有不同的表 示空间。问题表示的优劣，对求解问题及求解工作量的影响甚大。从问题表示到 问题的解决，有一个求解的过程，也就是搜索过程。在这一过程中，采用适当的 搜索技术，包括各种规则、过程和算法的推理技术，力求找到问题的解答。 ! 旦! ! 坠：! 茎王! 1 2 里塑! 坠：兰堡 一 下面介绍图搜索的一般策略，它给出图搜索过程的一般步骤，并可从中看来 无信息搜索和启发式搜索的区别。 可把图搜索控制策略看成是一种在图中寻找路径的方法。初始节点和目标节 点分别代表初始数据库和满足中止条件的数据库。求得把一个数据库变换为另一 个数据库的规则序列问题就等价于求得图中的一条路径问题。 图搜索( g r a p h s e a r c h ) 的一般过程如下： ( 1 ) 建立一个只含有起始节点s 的搜索图g ，把s 放到一个叫做o p e n 的未扩展节点表中。 ( 2 ) 建立一个叫做c l o s e d 的已扩展节点表，其初始为空表。 ( 3 ) l o o p ：若o p e n 表是空表，则失败退出。 ( 4 ) 选择o p e n 表上的第一个节点，把它从o p e n 表移出并放进 c l o s e d 表中，称此节点为节点n 。 ( 5 ) 若n 为一目标节点，则有解并成功退出，此解是追踪图g 中沿着 指针n 到s 这条路径而得到的( 指针将在第( 7 ) 步中设置) 。 ( 6 ) 扩展节点n ，同时生成不是n 的祖先的那些后继节点的集合m 。 把m 的这些成员作为n 的后继节点添入图g 中。 ( 7 ) 对那些未曾在g 中出现过的( 即未曾在o p e n 表或c l o s e d 表 上出现过的) m 成员设置一个通向n 的指针，把m 的这些成员加 进o p e n 表。对已经在o p e n 或c l o s e d 表上的每个m 成员， 确定是否需要更改通向1 1 的指针方向。对已在c l o s e d 表上的每 个m 成员，确定是否需要更改图g 中通向它的每个后裔节点的 指针方向。 ( 8 ) 按某一任意方式或按某个探试值，重排o p e n 表。 ( 9 ) g o l o o p 。 以上搜索过程可用如图1 - 1 所示的程序框图 1 2 】来表示。 4 b d d r p a * ：基十o b d d 的r p a 算法 图1 - 1 图搜索过程框图 这个过程一般包括各种各样的图搜索算法。此过程生成一个明确的图g ( 称 为搜索图) 和g 的一个子集t ( 称为搜索树) ，树t 上的每个节点也在图g 中。 搜索树是由步骤( 7 ) 中设置的指针来确定的。g 中的每个节点( s 除外) 都有 一个只指向g 中一个父辈节点的指针，该父辈节点就定为树中那个节点的唯一 父辈节点。搜索图形成局部的排序，因为图中没有一个后继节点是自己的祖先节 点( 见步骤( 6 ) ) 。到达由算法发现的某个节点上，每条可能的路径被明确地保 存在图中。对任何节点的单独一条明显路径是用t 来定义的；粗略地说，在o p e n 表上的节点都是搜索图的端节点，而在，c l o s e d 表上的节点则不是。较确切 b d d r p a * ：基于o b d d 的r p a + 算法 地说，在步骤( 3 ) ，o p e n 表上的前点都是搜索树上未被扩展的那些节点；在 c l o s e d 表上的节点，或者是几个已被扩展但是在搜索树中没有生成后继节点 的端节点，或者是搜索树的非端节点。 步骤( 8 ) 对o p e n 表上的节点进行排序，以便能够从中选出一个“最好” 的节点作为步骤( 4 ) 扩展使用。这种排序可以是任意的，即盲目的( 属于盲目 搜索) ，也可以用以后要讨论的各种启发思想或其他准则为依据( 属于启发式搜 索) 。每当被选作扩展的节点为目标节点时，这一过程就宣告成功，结束。这时， 能够重现从起始节点到目标节点的这条成功路径，其办法是从目标节点按指针向 s 返回追溯。当搜索树不再剩有未被扩展的端节点时，过程就以失败告终( 某些 节点最终可能没有后继节点，所以o p e n 表可能最后变成空表) 。在失败终止的 情况下，从起始节点出发，一定达不到目标节点。 g r a p h s e a r c h 算法同时生成一个节点的所有后继节点。为了说明图搜索 过程的某些通用性质，将继续使用同时生成所有后继节点的算法，而不采用修正 算法。在修正的算法中，一次只生成一个后继节点。 从图搜索过程可以看出，是否重新安排o p e n 表，即是否按照某个试探值 ( 或准则、启发信息等) 重新对未扩展节点进行排序，将决定该图搜索过程是无 信息搜索还是启发式搜索。 1 2 一般的搜索技术 知识的搜索与推理是人工智能研究的另一个核心问题。对这一问题的研究曾 经十分活跃，而且至今仍不乏高层次的研究课题。正如知识表示一样，知识的搜 索与推理也有众多的方法，同一问题可能采用不能的搜索策略，而其中有的比较 有效，有的不大适合具体问题。 在应用盲目搜索进行求解的过程中，一般是“盲目”地穷举，即不运用特别 信息。盲目搜索包括宽度优先搜索、深度优先搜索和等代价搜索等。其中，有界 深度优先搜索从某种意义上讲，具有一定的启发性。从搜索效率看，一般来说， 有界深度优先搜索较好，宽度优先搜索次之，深度优先搜索较差。不过，如果有 6 b d d r p a * ：基于o b d d 的r p a 算法 解，那么宽度优先搜索和深度优先搜索定能够找到解答，无论付出多大代价； 而有界深度优先搜索则可能丢失某些解。 启发式搜索主要讨论有序搜索( 或最好优先搜索) 、最优搜索a s 算法和a o s 算法。与盲目搜索不同的是，启发式搜索运用启发信息，引用某些准则或经验来 重新排列o p e n 表中节点的顺序，使搜索沿着某个被认为最有希望的前沿区段 扩展。正确选择估价函数，对于寻求最小代价路径或解树，至关重要。启发式搜 索要比盲目搜索有效得多，因而应用较为普遍。 有些问题的搜索既可以使用正向搜索，又可以使用逆向搜索，还可以混合从 两个搜索方向进行搜索，即双向搜索。当这两个方向的搜索边域以某种形式会合 时，此搜索以成功而告终。 1 3a + 算法 令估价函数厂使得在任意节点上其函数值f ( n ) 能够估算出从节点s 到节点 n 的最小代价路径的代价与从节点n 到某一目标节点的最小代价路径的代价之总 和，也就是说，( n ) 是约束通过节点1 1 的一条最小代价路径的代价的一个估计。 因此，o p e n 表上具有最t j x f 值的那个节点就是所估计的加有最小严格约束条件 的节点，而且下一步要扩展这个节点是最合适的。 在正式讨论a + 算法之前，先来介绍几个有用的记号。令k ( n i ，n j ) 表示任 意两个节点n f 和可之间最小代价路径的实际代价( 对于两节点间没有通路的 节点，函数k 没有定义) 。于是，从节点n 到某个具体的目标节点t i ，某一条最 小代价路径的代价可由k ( n ，t ) 给出。令 + ( n ) 表示整个目标节点集合 “ 上所有k ( n ， t f 中最小的一个，因此， + ( n ) 就是从1 3 到目标节点最小代价路径的代价，而且 从1 1 到目标节点能够获得舻( n ) 的任一路径就是一条从n 到某个目标节点的最佳 路径( 对于任何不能到达目标节点的节点n ，函数 + 没有定义) 。 通常感兴趣的是想知道从已知起始节点s 到任意节点1 1 的一条最佳路径的代 价k ( s ，n ) 。为此，引进一个新函数旷，这将使记号得到某些简化。对所有从s 开 始可达到n 的路径来说，函数旷定义为 b d d r p a * ；基于o b d d 的r p a 算法 g + ( n ) = g ( s ，n ) 其次，定义函数户，使得在任一节点n 上其函数值户( n ) 就是从节点s 到节 点n 的条最佳路径的实际代价加上从节点n 到某目标节点的一条最佳路径的代 价之和，即 广( n ) = 9 4 ( n ) + 扩( n ) 冈而广( n ) 值就是从s 开始约束通过n 的一条最佳路径的代价，而广( s ) = t ( s ) 是一条从s 到某个目标节点中间无约束的一条最佳路径的代价。 希望估值函数厂是广的一个估计，此估计可由下式给出： f i n ) = g ( n ) + ( n ) 其中g 是g + 的估计，h 是 + 的估计。对于“n ) 来说一个明显的选择就是搜索树 中从s 到n 这段路径的代价，这一代价可以在由从n 到s 寻找指针时，把所遇 到的各段弧线的代价加起来给出( 这条路径就是到目前为止用搜索算法找到的从 s 到n 的最小代价路径) 。这个定义包含了“n ) 矿( n ) 。 ( n ) 的估计 ( n ) 依赖 于有关阉题的领域的启发信息。这种信息可能与八数码难题中的函数w ( n ) 所用 的那种信息相似。把h 口q 做启发函数。 a 算法是一种有序搜索算法，其特点在于对估价函数的定义上。对于一般 的有序搜索，总是选择厂值最小的节点作为扩展节点。因此，是根据需要找到 一条最小代价路径的观点来估算节点的。可考虑每个节点1 1 的估价函数值为两个 分量：从起始节点到节点r 1 的代价以及从节点n 到达目标节点的代价。 在讨论a + 算法之前，先给出下列定义： 定义1 1 在g r a p h s e a r c h 过程中，如果步骤( 8 ) 的重排o p e n 表是 依赖贝x ) = 双x ) + ( x ) 进行的，则称该过程为a 算法。 定义1 2 在a 算法中，如果对所有的x 存在 ( x ) 体( x ) ，则称 ( x ) 为 船( x ) 的下界，它表示某种偏于保守的估计。 定义1 3 采用肺( x ) 的下界矗( x ) 为启发函数的a 算法，称为a 木算法。当 h = 0 时，斛算法就变为有序搜索算法。 a 木算法 ( 1 ) 把s 放入 ) p e n 表，记f = h ，令c l o s e d 为空表。 ( 2 ) 重复下列过程，直至找到目标节点为止。若o p e n 表为空表，则宣告 b d d r p a * ；基于o b d d 的r p a * 算法 失败。 ( 3 ) 选取o p e n 表中未设置过的具有最小，值的节点为最佳节点 b e s t n o d e ，并把它放入c l o s e d 表。 ( 4 ) 若b e s t n o d e 为一目标节点，则成功求得一解。 ( 5 ) 若b e s t n o d e 不是目标节点，则扩展之，产生后继节点s u c c e s s o r 。 ( 6 ) 对每个s u c c e s s o r 进行下列过程： ( a ) 建立从s u c c e s s o r 返回b e s t n o d e 的指针。 ( b ) 计算g ( s u c ) = 占( b e s ) + k ( b e s ，s u c ) 。 ( c )如果s u c c e s s o r o p e n ，则称此节点为o l d ，并把它添至b e s t n o d e 的后继节点表中。 ( d ) 比较新旧路径代价。如果g ( s u c ) 件( s ) 。 证明略。 引理1 2 ：a + 结束前，o p e n 表中必存在f i n ) 件( s ) 的节点( n 是在最佳路 径上的节点) 。 证明略。 定理1 2 ：对无限图，若从初始节点s 到目标节点t 有路径存在，则a + 也一 定能成功结束。 证明略。 推论1 1 ：o p e n 表上任一具有f i n ) h l ( n ) ，则在具有一条从s 到t 的隐含图上，搜索结 束时，由a 2 所扩展的每一个节点也必定由a 1 所扩展，即a 1 扩展的节点数至少 b d d r p a * ：基于o b d d 的r p a * 算法 和a 2 一样多。 证明略。 1 4 二叉决策图o b d d 通过符号化表示状态转移图 1 5 ，很多更大的系统都能被验证。新的符号化 表示是基于b r y a n t 的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 a m o 。o b d d 为和尔 公式提供了一种标准的表示方式，这种表示方式通常比合取范式或析取范式更紧 凑，而且也有非常有效的方法对它们进行操作。由于符号化表示很紧凑地描述了 由电路或协议决定的状态空间的规律性，所以有可能验证状态空间非常大的系 统。 最近十几年来，在符号化模型检测领域，基于b d d 表示的高效查找技术已 经发展起来，使得模型检测工具能够验证具有非常大的状态数目的系统。最近， b d d 被应用到知识表达和推理领域会，知识的模型检测及安全协议验证领域， 都取得了非常好的结果。尤其在文献中【1 7 】中使用了b d d 而使得知识表达和推 理取得很好的进展，可处理的问题规模得以大幅度提高。 下面我们描述怎样用二叉决策图符号化的表示有限状态系统。我们首先讨论 二叉决策图怎样被用来表示布尔函数。布尔函数被定义为在0 和1 上面，0 代表 f a l s e ，1 代表t r u e 。二叉决策图的大小跟变量的顺序有很大的关系。使用这种表达 方式各种逻辑操作能有效的实现。随后我们讨论如何用二叉决策图表示状态搜索 空间，这样我们就可以在计算机上实现基于o b d d 的算法。我们将看到利用二 叉决策图可以在很大程度上改进搜索算法。 有序二叉决策图( o b d d ) 是布尔公式的一种规范形式表示1 8 】。这种表示通 常比传统的合取范式或析取范式更紧凑，而且对o b d d 的操作也非常有效。因此 o b d d 广泛应用在计算机辅助设计中，包括信号模拟，组合逻辑验证，最近也开 始用于有限状态并发系统的验证。 为了讨论- - 3 ( 决策图，我们首先考虑如何生成一棵二叉决策树。二叉决策树 是一个有根的有向树，它由两类结点组成，终结点和非终结点组成。每一个非终 b d d r p a * ：基十o b d d 的r p a * 算法 结点v 由一个变量v a r ( v ) 标识，它有两个后继结点：l o w ( v ) 对应变量v 被赋值成 为0 的情况，h i g h ( v ) 对应变量v 被赋值为1 的情况。每个终端结点v 被表示为 v a l u e ( v ) ，v a l u e ( v ) 要么足0 要么是1 。 考虑布尔函数f ( a 1 ，a 2 ，b l , b 2 ) = ( a l b i ) ( a2 付b 2 ) 表示的二位比较器，该 比较器由布尔公式( a l 针b 1 ) ( a 2 b 2 ) 定义，其二叉决策树表示如图1 - 3 所示： 图1 - 3 ( a l 针b 1 ) ( a 2 付b 2 ) 的二叉决策图 从树的根结点出发到终端结点，我们可以确定该路径上对变量的真值赋值是 否使该二叉决策图表示的布尔公式为真。如果变量v 被赋值为0 ，那么从根结点 到终端结点的路径上的下一个结点将是l o w ( v ) 。如果v 被赋值为1 那么路径上的 下一个结点将是h i 曲( v ) 。标识终端结点的值是该布尔函数在此路径赋值下的值。 例如，赋值 通向标号为0 的叶子结点；因此布尔公式 ( a ，h b ，) ( a 2h b 2 ) 在这个赋值下为假。 二叉决策树并没有为布尔函数提供简明的表示，实际上，二叉决策图跟真值 表的规模大小相同。幸运的是，我们看到在二叉决策树中通常有许多冗余。例如， 图1 - 3 所示的二叉决策树中，有八棵根结点标识为b 2 的子树，但只有三棵子树 是不相同的。因此，合并同态的子树可以得到布尔公式的更简练的表示。合并的 结果是一个有向无环图，我们称之为二叉决策图。更准确的说，一个二叉决策图 是一个有根的有向无环图，它有两种结点，终端结点和非终端结点。与二叉决策 树相似，每一个非终端结点v 由一个变量v a t ( v ) 标记，有两个后继结点，l o w ( v 1 和h i g h ( v ) 。每一个终端结点标记为0 或1 。每个以v 为根的二叉决策图b 确定 一个布尔函数f 。( x 。，x 。) ，方法如下： b d d r p a * ：基ro b d d 的r p a + 算法 i 如果v 是一个终端结点 2 如果v a l u e ( v ) = l 那么f 。( x ，xn ) 2 1 。 3 如果v a l u e ( v ) = 0 那么f ，( x ”，x 。) 2 0 。 4 如果v 是一个非终端结点，v a r ( v ) = x i ，那么f v 是一个函数 f v ( x 1 ，x 。) = ( x 。k f l o w ( v ) ( x l ，x 。) ) v ( x ： f h 。g b ( 。) ( x l ，x 。) ) 。 在实际的应用中我们想要得到布尔公式的标准表示。这样一种表示必须具有 这样一种性质：两个布尔公式逻辑相等当且仅当它们有同态的表示。这个性质使 一些任务简化了，例如检查两个公式的相等和决定一个给定的公式是否可以满 足。如果两个二叉决策图满足下面的情况，我们说两个二叉决策图是同态：如果 存在一个一对一的函数h ，这个函数把一个终端结点映射到另一个终端结点上， 一个非终端结点映射到另个非终端结点上，对于每一个终端结点v ， v a l u e ( v ) = v a l u e ( h ( v ) ) 和对于每一个非终端结点v ，v a r ( v ) - - - v a r ( h ( v ) ) h ( 1 0 w ( v ) ) = l o w ( h ( v ) ) ，并且h ( h i g h ( v ) ) = h i 曲( h ( v ) ) 。 给二叉决策树加上两个约束我们可以得到布尔公式的标准表示。第一个约 束：对于每一条从根结点到终端结点的路径，变量都以相同的次序出现。第二个 约束：在图中没有同态和冗余的结点存在。第一个约束通过给标识二叉决策图结 点的变量一个全序，并且要求对于每一个图中的结点u ，如果u 有一个非终端的 后继v ，那么v a r ( u ) v a r ( v ) 。第二个约束通过重复运用三条转换规则达到，这些 转换规则并不修改这个图所表示的布尔函数： 删除重复的终端结点对于一个给定的标号删除至只有一个终端结点，并且 把所有的到被删除结点的弧重定向至那个剩余的结点。 删除重复的非终端结点对于两个非终端结点u 和v 有v a t ( u ) = v a t ( v ) t o w ( u ) = l o w ( v ) 和h i g h ( u ) = h i g h ( v ) ，那么把u 或v 删除，并把所有的入弧重定向 至另一个结点。 删除冗余的测试如果对于非终端的结点v 有l o w ( v ) = h i g h ( v ) ，那么删除v 并 且重定向所有的入弧至l o w ( v ) 。 从二叉决策图满足有序这个性质开始，通过不断应用转换规则直到图的大小 不再变小，我们得到标准形式。在 1 6 1 中向我们展示了以一种自底向上方式以 1 4 b d d r p a * ：基于o b d d 的r p a 4 算法 个被称为“归约”的程序实现转换规则。这个程序运行的时间与二义决策图大小 成线性关系。通过这种方式得到的图称为有序二叉决策图( o b d d ) 。例如，如果 我们对于二位比较函数使用顺序a l b l a 2 b 2 ，我们得到如图1 - 4 所示的o b d d 。 图1 - 4 ( a l b 1 ) a ( a 2 b 2 ) 的二叉决策图 不同的变量顺序对o b d d 的大小的影响是很大的。比如函数f = x ，x 2 v x 3 x t v x 2 1 x 2 ，如果按照x 1 x 2 x 。这样的顺序，它的o b d d 表示有线性的大小( 2 n + 2 个节点) ；而如果按照l ，3 ，2 n 一1 ，2 ，4 ，2 n 这样的顺序，它的0 b d d 就有指 数的大小( 2 “n + 1 个节点) 。不幸的是，给定一个函数，找到它的最佳变量顺序 的o b d d 表示是一个n p h a r d 问题。 2 9 中使用一些启发式策略对许多实际相关 例子找到了好的排序方法，能把指数增长的状态空间用线性增长的o b d d 表示。 如果o b d d 被用于表示布尔函数的标准形式，那么检查两个公式相等就会 被规约为检查两个二叉决策图是否同态。相似的，可满足性可以通过检查是否与 只包括一个被标号为0 的终端结点的o b d d 相同来确定。 我们随后解释怎样用o b d d 实现重要的逻辑操作。让我们从把一些布尔公式 中的一些参数x 。限定在常量b 的这个函数开始。这个函数由目x i 。b 表示，并且满足 q x i _ b ( x l ，x ) = “x l ，x i 1bx i ，x ) 如果f 被表示成个o b d d ，通过深度优先遍历f 的o b d d ，限制日x b 的 o b d d 能够很容易的计算出来。如果结点v 有一个指针指向结点w ，并且v a r ( w ) = x ， 如果b 是0 ，我们把指针用l o w ( w ) 代替，如果b 是1 我们把指针用h i g h ( w ) 代替。这 样得到的图可能不是标准形式的，为了得到表示日x 。 b 的o b d d ，我们对这个图 b d d r p a * ：基于o b d d 的r p a 算法 应用规约函数。 对于所有具有两个参数的十六个逻辑操作，能够很容易的用表示成o b d d 的布尔函数来实现。实际上操作是两个o b d d 参数的线性复杂度。有效实现这 些操作的的关键思想是s h a n n o n 扩展。 仁( x 目x i - o ) v ( x a qx j - 1 ) b r y a n t 为计算所有的1 6 个逻辑操作给定了一个统一的被称为a p p l y 的算法。 假设+ 是任意的具有两个参数的逻辑操作，f 和f 为两个布尔函数。为了简化算法 的扩展我们引入下面的符号： v 和v 分别是o b d d f 和f 的根 x = v a r ( v ) 并且x - - v a r ( v ) 我们考虑取决于v 和v 关系的几种情况。 如果v 和v 都是终端结点，那么f * f = v a l u e ( v ) 8 v a l u e ( v ) 如果x = x ，那么我们使用s h a n n o n 扩展 p r = ( - 1 x a ( f l x i o + f l x i 一o ) ) v ( x a ( t f l x i 1 ，f l x i 一1 ) ) 把这个问题分解成两 个子问题。这个问题被递归的解决。最后我们得到的o b d d 的根结点将是一个新 结点w ，v a r ( w ) = x ，l o w ( w ) 将是表示( q x i 04 f ，l x i 0 )o b d d ，h i g h ( w ) 将是表示 ( 司x i - 1 + f ，1 x 。 - 1 ) 的o b d d 。 如果x x ，那么f lx i 一0 = f lx i - l = f ，因为f 并不依赖于x 。在这种情况下 s h a n n o n 扩展简化为： f * f - ( 一x 八( 日x i 一o + f ，) ) v ( x 八( 司x i ( o o ) ，( o r ) 一 ( 1 0 ) ，( i o ) 一 ( 0 1 ) ，( 1 0 ) 一 ( “) 和( 1 1 ) 一 ( 1 0 ) 。相对应转换函数的o b d d 表示如下： 图2 - 2 转换函数的o b d d 表示 在这个滑动游戏中，我们通过对s 的特征函数应用t 来决定从s 在一步内可 达的所有位置的状态函数。也就是我们找所有可以使t 和s 的特征函数的与( ) 为真的后继x 。令中s 为集合s 的特征函数并且s o 初始化为 s 。我们想通过 中s i 来计算中s t + i 。这可通过使用存在量词( 丑) 来实现。这样，o s i + i ( x ) 可根据公式j 慢( t ( x ，x ) 八中s i ( x ) ) 来赋值，然后，从中s o 开始，我们可以 重复这个过程来计算中s t ，中s 。，中s a ，直到其中一个特征函数和目标位置有 一个非空的交集为止。到此我们就找到了一个解。因为s i + l 的域是x ，而我 们需要每步都改变x 和x 之间的变量，这对应于一个简单的指针替换而不必改 变0 b d d 。集合s t 包含了所有从初始状态开始在i 步到达的状态，这刚好对应了 搜索树的宽度优先搜索。 1 9 b d d r p a * ：基1 o b d d 的r p a * 算法 黎龠a 图2 - 3 中s o ，中s 1 ，m s 2 和o s 3 的o b d d s 剩下的问题就是如何实现存在量词( 莹) 。我们知道在布尔代数中有j x t f ( x ) 一f i x i = 0 v f f | x i = l 。我们需要0 ( x i ) a p p l y ，因为x i 被替换为常量c 可以用o b d d 的约束规则实现，每个带有索引i 的节点，( 1 - - c ) 后继被连向o - s i n k 。从图2 2 可以看出，我们可以通过直接计算o b d d 下半部分的根结点的或( v ) 做到更好。 最后，因为中s i 只涉及到可满足性，所以我们可以在一步内联合带存在量词的 t ( x ，x ) 和中s 。的与( 八) 。 出于容易处理的0 b d d s 大小的考虑，我们设置变量的顺序为x 和x 的交义 出现。把各个或子树与的递归计算的函数e x i s t a n d 如表2 - 1 所示 2 9 ： 表4 1j 菹( t ( x ，x ) 八o s i ( x ) ) 输入：0 b d d sg t ，g o 输出：o b 叻g 习，( t ( i 。，) &