（计算机软件与理论专业论文）基于局部搜索隐蔽集算法的qbf求解器研究.pdf

独创性声明 本人郑重声明：所提交的学位论文是本人在导师指导下独立进行研究工作所取得的 成果。据我所知，除了特别加以标注和致谢的地方外，论文中不包含其他人已经发表或 撰写过的研究成果。对本人的研究做出重要贡献的个人和集体，均已在文中作了明确的 说明。本声明的法律结果由本人承担。 学位论文作者签名：盎邀：童 日期： 砌乡i 弓 学位论文使用授权书 本学位论文作者完全了解东北师范大学有关保留、使用学位论文的规定，即：东北 师范大学有权保留并向国家有关部门或机构送交学位论文的复印件和电子版，允许论文 被查阅和借阅。本人授权东：i l ：n 范大学可以采用影印、缩印或其它复制手段保存、汇编 本学位论文。同意将本学位论文收录到中国优秀博硕士学位论文全文数据库( 中国 学术期刊( 光盘版) 电子杂志社) 、中国学位论文全文数据库( 中国科学技术信息研 究所) 等数据库中，并以电子出版物形式出版发行和提供信息服务。 ( 保密的学位论文在解密后适用本授权书) 学位论文作者签名：缸 日 期：趁丝：堡 学位论文作者毕业后去向： 工作单位： 通讯地址： 指导教师签名： 日期： 电话： 邮编： 摘要 智能规划是人工智能中比较热门的研究领域之一，目前智能规划求解的主要方法之 一是将智能规划问题转化为命题可满足问题( p r o p o s i t i o n a ls a t i s f i a b i l i t yp r o b l e m ，简称 s a t ) ，然后利用高效的s a t 求解器进行求解。 命题可满足性问题( 简称s a t ) 是当今人工智能研究的核心问题。s a t 问题可以 描述为给定一个命题逻辑公式，其变元是否存在一个真值赋值使命题公式成立( 可满 足) ，如果成立则返回这些变元的真值赋值。s a t 问题是比较难求解的问题，其计算复 杂性是n p 完备的，而实例的隐藏结构能够找到有效的s a t 求解方法，b a c k d o o r s 就是 这种隐藏结构之一。 隐蔽集( b a c k d o o rs e t s ) 是s a t 问题的一个重要韵隐藏结构，与问题难度有很大的关 系。它的选择能使剩下的问题在多项式时间内求解。隐蔽集可以描述为一个较小的变量 子集口，对b 中的变量进行真值指派后，简化后的公式可以在多项式时间内求解。由于 其在复杂问题求解中的重要性，近年来隐蔽集的研究已逐步成为研究的热点。目前隐蔽 “ 集的求解方法已经扩展到q b f 问题中。! 严? 量化布尔公式( q u a n t i f i e db o o l e a nf o r m u l a e ，简称q b f ) 是一种带有存在量词和全称 量词前缀的命题逻辑公式。当q b f 公式中的量词中只含存在量词时，q b f 问题就转化 ，为s a t 问题。因此q b f 问题可以看作是s a t 问题的泛化。q b f 问题是比s a t 问题更 加难解的问题，其计算复杂性是p s p a c e 完备的。隐蔽集的引入能提高q b f 问题的求 解效率。 本文首先对现有的隐蔽集问题的求解算法进行一个总体的概述，其次针对q b f 问 题设计了一种新的基于重命名的隐蔽集求解算法，并将隐蔽集首次应用到的q b f 求解 器中从而设计出一种新的b d q b f 求解器。在b d q b f 中，我们用隐蔽集中的变量作启 发式，引导算法进行分支搜索，从而减小了算法的搜索空间和回退次数，并提高了q b f 问题的求解效率。最后本文针对这一算法进行了两类实验：第一类实验是在w i n d o w s 环境下用标准的c + + 实现这一算法，并与原有求解q b f 问题的隐蔽集算法进行了比较， 结果表明这一算法能求解出问题的较小隐蔽集；第二类实验是在l i n u x 环境下用标准 c + + 语言实现了q b f 问题求解器b d q b f 系统。结果表明无论是q b f 的随机问题还是 标准测试间题，b d q b f 求解器都有很好的求解效果。这些实验验证了隐蔽集在q b f 问 题求解中的实际价值。 关键词：智能规划；q b f 问题；q b f 问题求解器；隐蔽集；局部搜索；重命名 r 靠 ， a b s t r a c t r e c e n t l y ，i n t e l l i g e n tp l a n n i n gi sf o c u s e do nt h em o r ea n dm o r er e s e a r c h e r si na r t i f i c i a l i n t e l l i g e n c ef o c u so n u pt ot h ep r e s e n t ，o n eo f t h ei m p o r t a n ta p p r o a c ho fs o l v i n gi n t e l l i g e n t p l a n n i n gi sc o m p i l e dp l a n n i n gp r o b l e mt os a tp r o b l e m ，a n dt h e nu t i l i z i n gh i g he f f i c i e n ts a t s o l v e rt or e s o l v ei t n ep r o p o s i t i o n a ls a t i s f i a b i l i t yp r o b l e m ( s a t ) i sa ni m p o r t a n ti s s u e i na i g i v e na p r o p o s i t i o n a ll o g i cf o r m u l a , t h ep r o p o s i t i o n a ls a t i s f i a b i l i t yp r o b l e m ( s a t ) i sap r o c e s so f d e c i d i n gt h es a t i s f i a b i l i t y t of o r m u l a s a tp r o b l e mi sm o r ed i f f i c u l tt os o l v e ，i e w h i c h c o m p u t a t i o n a lc o m p l e x i t yi sn p c o m p l e t e 1 1 1 eh i d d e ns t r u c t u r eo fi n s t a n c e s - ab a c k d o o rs e t o f v a r i a b l ec a ni m p r o v et h ee f f i c i e n c yo fs a t p r o b l e m o n ee x a m p l eo fs u c hh i d d e ns t r u c t u r ei sab a c k d o o rs e to fv a r i a b l ef o rs a t , w h i c h c a p t u r e st h el i n kb e t w e e nd e p e n d e n c i e sa m o n gb a c k d o o r v a r i a b l e sa n dp r o b l e mc o m p l e x i t y a b a c k d o o rs e to ff o r m u l afi sas u b s e tbs u c ht h a ti ft h ea s s i g n st ot h ev a r i a b l e si nbc e r t a i n t r u t hv a l u e s ，t h e nt h es i m p l i f i e di n s t a n c eb e l o n gt oac l a s sco fi n s t a n c e st h a fc a nb es o l v e di n p o l y n o m i a lt i m e b e c a u s eo fi t si m p o r t a n c ei ns o l v i n gc o m p l e xp r o b l e m s ，t h er e s e a r c ho f b a c k d o o r sh a sb e c o m er e s e a r c hf o c u si nr e c e n ty e a r s t h em e t h o do fs o l v i n gb a c k d o o r sh a s 。b e e ne x t e n d e dt ot h eq b fp r o b l e mc u r r e n t l y q u a n t i f i e db o o l e a nf o r m u l a ec a nb es e e na st h eg e n e r a l i z a t i o no fs a t i s i a b i l i t y ( s a t ) 、 ，i t l le x i s t e n t i a lo ru n i v e r s a lq u a n t i f i e r st oe v e r yv a r i a b l eo fp r o p o s i t i o n a lf o r m u l a e q b f p r o b l e mi sm o r ed i f f i c u l tt os o l v et h a ns a tp r o b l e m ，i e w h i c hc o m p u t a t i o n a lc o m p l e x i t yi s p s p a c e ，a n dw h i c hp l a y sa ni m p o r t a n tr o l e i na i n ei n t r o d u c t i o no fb a c k d o o r sc a n i m p r o v et h ee f f i c i e n c yo fq b f p r o b l e m i nt h i sp a p e r , w eg i v eag e n e r a lo v e r v i e wo ft h ee x i s t i n ga l g o r i t h m so fab a c k d o o rs e tf o r p r o b l e mi n s t a n c e s ，t h e np r e s e n tan e wa l g o r i t h mo fc o m p u t i n gb a c k d o o rs e tf o rq b fb a s e so n r e n a m e dv a r i a b l ea n du s et h eb a c k d o o rs e tt oq b fs o l v e rf o rt h ef i r s tt i m et od e s i g nan e w q b fs o l v e r b d q b fs y s t e m a c c o r d i n gt ot h ep r o c e s so fc o m p u t i n gt h eb a c k d o o rs e t , b d q b fc a l ls e l e c tab r a n c hm o r ee x a c t l y , a n dt h i sc a nr e d u c et h es e a r c hs p a c ea n dt h e n u m b e ro fb a c k o f fo fq b fp r o b l e m ，a n dt h e ni m p r o v et h ee f f i c i e n c yo fs o l v i n gq b f p r o b l e m s f u r t h e r m o r e ，w ei l l u s t r a t e t h ea d v a n t a g e so fo u ra l g o r i t h mt h r o u g hs e v e r a l r e a l - w o r l dq b fi n s t a n c e s 1 1 1 ee x p e r i m e n t sa r ec a r r i e do u to nv c * o p e r a t i o np l a t f o r ma n d r e d h a te s 3 0 e x p e r i m e n t a lr e s u l ts h o wt h a tt h i s a l g o r i t h m c a l lc o m p u t et h es m a l l e r b a c k d o o rs e t sf o rq b fp r o b l e m sa n dt h eb a c k d o o rs e t sc o m p u t e dc a ni m p r o v et h ee f f i c i e n c y o fs o l v i n gq b f p r o b l e m s k e yw o r d s ：a r t i f i c i a lp l a n n i n g ；q u a n t i f i e db o o l e a n f o r m u l a ep r o b l e m s ；q b fs o l v e r ； b a c k d o o rs e t s ；l o c a ls e a r c h ；r e n a m a b l eh o r nc l a u s e i i i 目录 摘要 a b s t r a c t ： 目录 第一章引言 1 1 研究背景。： 1 2 本文的主要工作 1 3 论文的结构 第二章智能规划 2 1 智能规划的概念。 2 2 智能规划的应用 一笏2 ；- 1 航空航天领域中的应用 2 2 2 机器人领域中的应用： 2 2 3 智能工厂中的应用 2 2 4 商业中的应用 2 3 智能规划的主要求解方法 第三章s a t 问题、q b f 问题和b a c k d o o r 集合 3 1 相关概念- 3 2 隐蔽集的发展概况 3 3s a t 问题的隐蔽集 3 3 1 基于d l l 的求解算法 3 3 2 基于h o r n 公式的求解算法 3 3 3 基于r h o r n 公式的求解算法 3 3 4 基于2 c n f 公式的求解算法 3 4q b f 问题的隐蔽集 3 4 1 基于( h o r n 公式的求解算法 3 4 2 基于q 2 c n f 公式的求解算法o 第四章求解q b f 问题的b a c k d o o rs e t 算法框架： 4 1 局部搜索及公式重命名 4 2 求解o b f 问题的隐蔽集算法 第五章算法设计与实现 5 1r q h o r n - b a c k d o o r 5 1 1r q h o r n b a c k d o o r s 的求解算法实现 i v 5 1 2 实验比较2 2 s 2b d q b f 系统与已有q b f 求解器q u e f f l e 的比较2 3 第六章总结2 6 参考文献2 7 致谢3 0 在学期间公开发表论文情况31 v 东北师范大学硕士毕业论文 第一章引言 1 1 研究背景 智能规划是人工智能中的一个重要的研究领域。简单地说智能规划的主要思想是在 初始条件下，对对象实施怎样的操作，才能使问题的目标得以实现。智能规划是一个交 叉研究领域，它涉及知识推理、非单调逻辑和人机交互等多个方面。本章将主要介绍智 能规划的一些相关概念。 智能规划的求解方法有很多种，目前规划求解的主要方法之一是将规划问题编译为 命题可满足问题( s a t 问题) ，然后利用高效的s a t 求解器进行求解。1 9 9 2 年k a u t z 等 人第一次把规划问题求解转化为s a t 问题求解，该方法使得s a t 求解的新技术可以直 接应用于规划系统，从而有效地推动了规划研究。s a t 问题是比较难求解的问题，其计 算复杂性是n p 完备的，研究实例的隐藏结构能够找到有效的求解s a t 问题的方法，隐 蔽集就是这种隐藏结构之一。所以隐蔽集问题的研究在规划领域中具有相当重要的理 论价值和现实意义。 量化布尔公式【1 ( q u a n t i f i e db o o l e a nf o r m u l a e ，简称q b f ) 是一种带有存在量词和全 称量词前缀的命题逻辑公式。当q b f 公式的量词中只包含存在量词时，q b f 问题就转 化为命题可满足( s a t ) p 题。故q b f 问题可以看作s a t 问题的泛化。q b f 问题的可满 足性是判定一个给定的量化布尔公式是否存在一组命题变量的真值指派，使得公式在该 真值指派下为真。目前大多数求解q b f 问题的方法都是扩展原有的s a t 问题求解的方 法：g e n t 等人将s a t 问题求解器w a l k s a t 启发式方法1 2 j 扩展到q b f 求解器w a l k q s a t 中，使得q b f 的求解效率有了一定的提高；r o w l e y 等人将s a t 求解器z c h a f f 中的监 视文字【3 】应用到了q b f 求解器w a t c h e d c s b j ，其使用的数据结构是通过扩展s a t 求 解器z c h a f f 中所使用的监视文字而得到的：g i u n c h i g l i a 等人扩展s a t 求解算法d p l l 【4 j 从而设计出一种新的q b f 求解器q u a e ，它所使用的数据结构和w a t c h e d c s b j 一样， 同时其子句学习技术也参考了z c h a f f 中的子句学习技术；r i n t m l e n 等人参考s a t 求解 器c s a t 中所使用的m o m s 方澍5 】从而设计出q s a t 求解器；z h a n g 等人采用s a t 求 解器z c h a f f 中的变量状态独立衰退总和方法设计出q u a f f l e 求解器，其子句学习技术直 接利用了z c h a f f 中所用的子句学习技术 6 1 。 隐蔽集【7 】可以看作一个较小的变量子集，与问题难度有很大的关系，隐蔽集中变量 的真值指派能使得简化的公式在多项式时间内求解。对于现实中的一个s a t 问题实例来 说，如果已知它的隐蔽集召，那么至多运行2 旧次多项式算法就可以判定该s a t 问题的 可满足性。换言之，用隐蔽集中的变量作为求解s a t 问题中的分支变量可以使s a t 求 解器达到较好的求解效果。b s e l m a n 等人在2 0 0 3 年提出了隐蔽集【7 】的概念并用实验的 东北师范大学硕士毕业论文 方法证明现实实例中存在一些较小的隐蔽集；由于隐蔽集与问题难度有很大的关系，近 年来求解隐蔽集这一问题成为研究的热点之一。 目前求解s a t 问题的隐蔽集的方法已有很多，例如：2 0 0 4 年s s z e i d e r 等人提出一 种求解隐蔽集的f p t 算法【8 】，该算法是基于多项式时间内可解的基本类( h o r n 公式， 2 c n f 公式) 的；2 0 0 5 年s s z e i d e r l 9 1 等人又提出一种基于d l l 子求解器的一种求解隐 蔽集的方法，t w a l s h 等人从理论和实验的角度分析了隐蔽集和骨架( b a c k b o n e ) 间的 关系，并提出一些计算隐蔽集的方法【l o 】；2 0 0 6 年p s i e g e l 等人利用l o c a ls e a r c h 思想来 求解隐蔽集，并将隐蔽集应用到z c h a f f 求解器中使其求解效果有了很大的提升1 1 1 ；2 0 0 7 年s s z e i d e r 等人【1 2 】将隐蔽集推广到q b f 问题中，提出了基于多项式时间内可解的基本 类( q h o m 公式和q 2 c n f 公式) 的隐蔽集算法。 2 0 0 8 年s s z e i d e r 1 3 j 考虑隐蔽集中变 量间的关系，提出b a c k d o o rt r e e 的概念，并用实验的方法证明b a c k d o o rt r e e s 的叶节点 节数少于隐蔽集中变量的个数等等诸如此类的方法。 由于隐蔽集的定义是基于基本的可解类( 多项式时间内可求解的问题类) ，所以只要 找到一个问题的隐蔽集，就可以使该问题变得容易求解。目前求解q b f 问题的隐蔽集 方法还不是很多，只有一种2 0 0 7 年s a m e r 和s z e i d e r 2 7 1 提出的求解q b f 问题的 q h o m b a c k o o r s 和q 2 c n f b a c k d o o r 的算法。另外还没有将隐蔽集应用到q b f 。求解器 中，就这一现象本文提出了一种新的求解q b f 问题的隐蔽集算法，并用实验的方法表一。 明这一算法能求解出现实实例中q b f 问题的较小隐蔽集；同时将隐蔽集应用到q b f 求 解器中，以隐蔽集中的变量作为分枝变量来减小求解问题的搜索空间，从而提高求解问 题的效率。 1 2 本文的主要工作 1 本文首先对目前求解问题的隐蔽集方法进行了综合概述； 2 其次在已有的求解隐蔽集算法的基础上中设计一种新的求解q b f 问题的隐蔽集 的算法：基于重命名的q b f 问题的隐蔽集算法； ( 1 ) 重命名h o r n 公式可以看作逻辑命题公式中变量的一个真值指派，即通过翻转 一些变量的文字( 用x ( 吨) 取代子句中出现的川( x ) ) ，使得翻转后的公式变为h o r n 公式 1 3 9 , 4 0 。其基本思想是：首先利用局部搜索寻找q b f 子句集的最大可重命名r m 舣，这里 只需对存在变量进行重命名，这样可以确保重命名后q b f 公式中含有最多的h o r n 子句 数；其次根据懈对q b f 公式进行重命名得到新的q b f 公式少。 ( 2 ) 隐蔽集是一个变量集b ，对b 中的变量进行真值指派，简化公式f 可以在多 项式时间内被求解。其基本思想是：首先从q b f 命题公式中选择非h o r n 子句中出现最 多的变量x ，将x 的三角依赖变量并入集合b 中，之后简化q b f 命题公式；其次重复上 一步直到q b f 公式是q h o m 公式，由于q h o m 公式是多项式时间内可解的类，故求得 的b 是h o r n b a c k d o o r 2 东北师范大学硕士毕业论文 3 最后本文就这一算法做了两类实验。第一类实验结果表明该方法能求解出问题 的较小b a c k d o o r s 变量；同时根据这一算法设计一种新的q b f 问题求解器b d q b f ，并 用实验的方法表明该求解器的求解速度快予目前求解效率较高的q b f 求解器q u a f f i e 。 1 3 论文的结构 第一章介绍了本文的研究背景、主要工作及论文结构。 第二章介绍了智能规划的相关概念、智能规划的应用及智能规划的发展。 第三章介绍了命题可满足性问题、量化布尔公式及隐蔽集的相关概念，同时介绍了 目前比较流行的求解s a t 问题的隐蔽集方法和求解q b f 问题的隐蔽集方法。 第四章介绍重命名和局部搜索的相关概念，随之提出基于重命名的q b f 问题的隐 蔽集求解方法，并设计一种新的q b f 求解器b d _ q b f 。 第五章用实验的方法表明这一算法能求解出问题的较小隐蔽集变量，同时将隐蔽集 应用到q b f 求解器当中，与目前q b f 大赛上求解效果较好的q u a f f i e 求解器进行比较， 实验结果表明这一求解器能够较快地求解出问题的解。 第六章对全文进行总结，并指出将来要做的工作 4 j r p + 3 东f l t o 币范大学硕士毕业论文 第二章智能规划 智能规划是人工智能研究领域的一个重要分支，其发展对计算机科学、人工智能、 认知科学等领域产生了重要的影响，并在机器人、自然语言理解、知识推理、人机交互、 等方面存在广泛的应用。智能规划的主要思想是根据预先制定的目标，对周围环境进行 认识与分析，对若干可供选择的动作及提供的资源限制施行推理，综合制定出实现目标 的一个动作序列，这一动作序列就是一个规划( p l a n ) 。 近年来，智能规划的研究受到众多学者们的关注，已成为人工智能研究领域的一个 热点研究之一。在国外，一些专门从事智能规划研究方面的协会和联盟陆续成立；国际 知名期刊人工智能刊期( j o u r n a lo f a r t i f i c i a li n t e l l i g e n c e ，j a i ) 于19 9 5 年、2 0 0 3 年、 2 0 0 8 年三次以专刊的形式发表智能规划相关的研究成果，且发表的有关智能规划方面的 文章呈逐年增长的趋势；智能规划方面的学术会议也越来越多，这些迹象足以说明智能 规划已成为人工智能领域的一个研究热点。 本章主要介绍智能规划的一些相关概念、主要应用及其发展历程。 。 2 1 智能规划的概念 人们对智能规划的研究从1 9 5 6 年到现在已有半个多世纪了，m c d e r m o t t 和j a m e s h e n d e l e r 认为“规划就是设计某个实体( e n t i t y ) 的动作序列，其结果被称为规划解( p l a n ) 。 d e e p a kk u m a r 更加形象地说“p l a n n i n g = h o wd oig e tf r o mh e r et ot h e r e ? 。智能规划的 主要思想可以描述为根据预先制定的目标，认识和分析周围环境，对若干可供选择的动 作及提供的资源限制施行推理，从而制定出实现目标的一个动作序列，这一动作序列就 是一个规划( p l a n ) 。一个规划解实质就是实体执行的一个动作序列，如果一个实体在初 始状态下经过执行这一系列动作最终到达目标状态，那么这一系列动作( 动作的序列) 就叫做一个规划1 2 3 1 。一个规划问题( p l a n n i n gp r o b l e m ) 包括四个集合，分别为操作 ( o p e r a t o r s ) 集合、对象( o b j e c t s ) 集合、初始条件( i n i t i a lc o n d i t i o n s ) 集合和目标( g o a l s ) 集合，其中初始条件集合和目标集合的每个元素都是一个命题智能规划的目的就是寻 找一个从初始条件到目标得以实现的一个动作序列，找到的该动作序列就称规划解研 究智能规划的主要目的是建立高效实用的智能规划系统。该智能规划系统的主要功能可 以描述为：给定问题的初始状态描述、对状态描述进行变换的一组操作、初始状态和目 标状态。智能规划系统能够给出从初始状态到达目标状态的一个操作序列，其复杂性与 实体的功能及实体所处的环境有关。 广、 求解规划解的系统称为规划器，它是一种应用软件。给定问题的初始状态、目标状 态、相关操作和操作所使用的对象，规划器可以自动给出从初始状态到达目标状态的一 4 东北师范大学硕士毕业论文 个动作序列，即规划解，使得a g e n t 可以实现目标。评价规划器的标准是在尽可能短的 时间里，求解出高质量的最优规划解。所以规划算法的设计在规划器中占用重要的地位， 目前规划算法的研究已经是一个热门问题，使得规划问题的理论研究达到了一个新的高 度。 2 2 智能规划的应用 规划问题的研究已持续了四十多年。在这些年里，规划研究经历了从理论到应用、 从简单到复杂等过程。由于转变了智能规划的研究对象和研究方法，使智能规划的应用 领域得到了极大的扩展。目前自动系统中的智能规划，更加灵活和健壮，其适应性也得 到显著的提高。特别是在机器人、航空航天、智能企业和商业软件中，智能规划得到了 很广泛的应用。 2 2 1 航空航天领域中的应用 美国宇航局的a s p e n ( a u t o m a t e ds c h e d u l i n ga n dp l a n n i n ge n v i r o n m e n t ) u 副规划系统 在航天航空应用中取得最好的效果，a s p e n 是一个基于面向对象的系统，提供了一组 可重用的软件部件，主要包括约束模型语言、约束管理系统、搜索策略、一种语言、修 正规划能力、时序推理系统、图形化规划和调度的界面，这些部件可以比较简单地应用 在目前比较复杂的规划系统上。a s p e n 结合宇航器操作约束、宇航器硬件模型、飞行 规范、科学实验目标和操作过程来自动生成较低层次的宇航器操作序列。a p s e n 通过 自动生成宇航器操作序列与相关领域的知识相结合，使得宇航任务可以由一个小分队来 控制，以此来降低开销。智能规划在宇航器中的应用主要是将工程操作指令和较高层次 的科学研究转化为较低层次的宇航器执行指令。 2 2 2 机器人领域中的应用 智能规划在机器人学中具体的应用方向主要有：环境模型的描述，控制知识的表示， 路径规划，任务规划，协调操作( 运动) 规划，基于传感信息的规划等。目前主要研究领 域包括： 1 、路径规划：在满足动态约束的前提下，机器人能如何从一个初始的位置走到目标 位置的控制机制。 2 、感知规划：根据系统的感知如何采集内部信息和外部信息，如：确定机器人位置 和辨别物体对周围环境的观察。 3 、任务规划：是在动态的环境、不确定的或部分已知的状态条件下进行规划，其更 加注重资源和时间的分配。 4 、规划交流：是指人与机器人之间或多个机器人之间如何进行信息交换，主要包括 询问信息和反馈信息。 5 - 东北师范大学硕士毕业论文 2 2 3 智能工厂中的应用 智能化工厂中的智能规划主要采用资源约束的方法进行求解，是指从生产设计到监 测生产的一系列过程，它不仅可以是单个企业，还可以处理多个企业间的关系。 目前主要研究领域包括生产流程规划和生产安排规划和调度。 1 生产流程规划：在一个功能化的工厂中，生产流程规划先将现实生产流程转化 为知识库中信息，然后再根据相应的生产要求进行转化。在这方面取得较好效果的有基 于知识工程的软件。 2 生产安排规划和调度：为了按时交货，安排迎合客户需求的生产，与我们通常 所说的e r p 作业调度相似。 2 2 4 商业中的应用 商业中智能规划的应用对经典规划作了很大的扩充，其目标状态可以是满足某个条 件不是明确的命题，。 目前主要研究领域包括网络信息集成和运输规划。 1 网络信息集成：是为网络信息提供一种理解和重新组织的机制，根据领域本体 的内容，采集互联网上信息并集成这一信息到领域本体。目前在查询规划上得到了广泛 的应用。查询规划是将对信息对象框架的查询转化成只对信息源作访问的操作序列。在 规划的执行过程中，有时需要总体分析合并信息源返回的结果以便做出下一步的规划。 所以查询规划中的重要环节是信息的合并。信息的合并可以定义为：将两个残缺信息对 象的框架合并到一起。信息源之间的相关链接是合并的依据。 2 运输规划：在工厂作业调度规划问题中，对有限辆的货运汽车，在不同的地点之 间运送货物在汽车尽可能地满载，空车运行情况尽可能少，车辆闲置的情况尽可能少 的情况下，会给运输公司带来可观的效益即规划的输出就是一张车辆运转计划表， m u r p h y 等人1 9 9 6 年1 月为美国联帮太平洋铁路建立的铁路自动调度系统( r a i lt r a i n s c h e d u l e gr t s ) ，r t s 能够产生好的，低费用的调度计划【6 引美国联帮太平洋铁路由于使 用了这个调度系统，每年可节约资金5 0 万美元。 2 3 智能规划的主要求解方法 智能规划理论是在2 0 世纪5 0 年代后期迅速发展起来的一个前沿研究领域，至今它 的研究已达半个世纪之久，其发展对计算机科学、认知科学、人工智能等领域产生了重 要的影响，并广泛应用于机器人、知识推理、人机交互、自然语言理解等方面。目前规 划的求解方法有很多种，其主流方法之一是把规划问题编译成s a t 问题，然后利用高效 的s a t 求解器进行求解。 规划领域的三种新的求解方法使该领域取得革命性的发展。该三种方法分别为： 1 9 9 2 年k a u t z 等人把规划问题转化为命题可满足性问题，该方法使得命题推理系统中的 6 东北师范大学硕士毕业论文 新技术可以直接应用于规划系统，从而有效地推动了规划研究；1 9 9 5 年由b l u m 和f u r s t 提出的图规划【2 3 】【1 7 1 ，该方法第一次采用图的方式来解决规划问题，开辟了规划求解的新 途径；1 9 9 8 年由b o n e t 和g e f f n e r 提出的启发式方法 i s j ，它利用启发式函数来指导状态 空间搜索，表现出很强的问题求解能力。基于这三种方法的规划器在两年一度的国际规 划器竞赛中屡获冠军，表现出优异的性能。 7 l 东北师范大学硕士毕业论文 第三章s a t 问题、q b f 问题和b a c k d o o r 集合 1 9 9 2 年k a u t z 等人把规划问题转化为命题可满足性问题，这种方法使得命题推理系 统中的新技术可以直接应用于规划系统，从而有效地推动了规划研究；而q b f 问题通 常可以看作是s a t 问题的泛化。目前大多数q b f 问题求解器都是在扩展原有的s a t 问 题求解器的基础上设计的。隐蔽集是s a t 、c s p 等问题的一个重要的隐藏结构，它与问 题难度有很大的关系。隐蔽集可以有效地指导问题求解的搜索空间，从而加速求解速度， 同时可以使原来难求解的问题变为容易求解的子问题，隐蔽集的研究对于问题求解理论 的发展有着重要的意义。针对这一情况，国内外许多研究人员开始寻找求解隐蔽集的方 法，隐蔽集的求解成为一个研究热点。目前求解s a t 问题的隐蔽集方法很多，而求解 q b f 问题的隐蔽集方法只有一种。本部分主要介绍s a t 问题、q b f 问题、隐蔽集的相 关概念，及目前存在的s a t 问题的隐蔽集求解方法和q b f 问题的隐蔽集求解方法。 3 1 相关概念 s a t 2 2 】问题是命题可满足性问题的简称，即判定一个给定的命题逻辑公式是否可满 足，其中命题逻辑公式是指合取范式f ，它由子句合取组成，子句由文字析取组成。1 9 7 1 年c o o k 首次证明了s a t 问题是n p 完全的f 1 9 2 0 1 ，几乎所有n p 完全问题都可以在多项 式时间内归约到s a t 问题。研究表明，将许多n p 完全向题转化成s a t 问题进行求解 都比直接求解更方便更快捷。因此这个问题是计算复杂性理论的核心，在许多领域都有 非常重要的意义。 定义3 1 1 命题可满足问题( s a t ) 给定一个命题逻辑公式f ，其变量集为x = v a r ( f ) ， 是否存在对其变元x 的一个真值赋值使命题公式，成立( 可满足) ，如果成立则返回这 些变元的真值赋值。 量化布尔公式【2 3 1 ( q u a n t i f i e db o o l e a nf o r m u l a e ，简称q b f ) 是一种带有存在和全称量 词前缀的命题逻辑公式。一般情况下量化布尔公式y 可表示如下：q l x l gx n f ，其中 9 f r 髟3 1 ，i = l ，蠢f 即可以用合取范式表示也可以用析取范式表示，文中f 采用合取范 式，v a r ( f ) = “，x 2 ， ，对于任意的布尔变量葺( i = l ，刀) ，有且仅有一个量词对它进 行约束，由全称量词约束的变量称为全称变量，由存在量词约束的变量为存在变量。量 化布尔公式的可满足性问题是指给定一个量化布尔公式，判断是否存在一个解释，使得 该量化布尔公式在该解释下为真。如果存在该公式的一个解释使得该公式为真，则该公 式是可满足的( s a t ) ；否则是不可满足的( u n s a t ) 。需要注意的是，对于一个q b f 公式 q 卜q ，而f ，其量词顺序不可改变，例如公式v a 3 b ( a v6 ) ( 1 口v - ，b ) 和公式 8 东北师范大学硕士毕业论文 v b 3 a ( a v 6 ) ( - 1 口v - - , b ) 是逻辑不等价的。但是如果相邻的量词是相同的，可以交换量词 的顺序，例如v a 3 b 矽兰v b 3 a 矽，v a v b 矽兰v b v a 妒因此通常将相邻的相同量词合并， 这样公式可表示为： y = q 出么f( 1 ) 其中蜀是具有相同量词的变量集由于相邻的相同量词都在一组，这时公式( 1 ) 中的全称量 词和存在量词是交替出现的，每个量词约束一个变量集，文中q b f 公式采用形式( 1 ) 。其 中f 用子句集表示。例如公式v a 3 b ( a v b ) ( - - a v - - , b ) ，f = ( 口，6 ) ，( - 1 口，- 1 6 ) ) 记为q b f 子 句集。对每个子句c f 用v a r ( c ) 表示子句c 中出现的变量集合，v a r ( f ) = u c 。fv a t ( c ) 表 示f 中出现的所有变量集合。q b f 公式中出现的变量集可以表示为 v 鲫缈) = v a r ( f ) = u c 。f v a r ( c ) 。对q b f 公式中的变i t x , v a r ( 1 f f ) ，用屯( 而) = f 表示变量t 的 深度，即变量置在前辍量词中出现的次序。 对一个c n f 公式f 和一个变量子集v v a r ( f ) ，用f v = c ( 矿u 矿) ) 简化公式凡 其中矿= - ：z 研。相应地对一个q b f 公式y = q 置f 和一个变量集v v a r 缈) ，用y 一矿 简化公式y ，其中q b f 子句集f 用f y 取带，同时去除多余的量词；q b f 公式的评 价函数y 是一个 谚j ) 的映射，它是一个递归定义式，初始条件为：如果y = 矽，置 y ( y ) = 1 ；否则置 ，( y ) = 0 ；对任意变量x ，置y ( 比y ) = m i n ( v ( y 卜= o 】) ，y ( y 卜= 1 】) ) ； 对存在变量x ，置y ( 五y ) = m a x ( v ( y x = 0 】) ，y ( y h = 1 】) ) 。 如果q b f 公式的评价函数值为1 ，则表示q b f 公式是可满足的；如果q b f 公式的 评价函数值为0 ，则表示q b f 公式是不可满足的。如果两个q b f 公式的评价函数值相 等，那么这两个q b f 公式是等价的。 隐蔽集是s a t 、c s p 等问题的一个重要的隐藏结构，与问题难度有很大的关系，它 的求解能使较难问题的求解变得比较容易求解。目前存在三种相关的隐蔽集，分别为强 隐蔽集、弱隐蔽集和删除隐蔽集。 定义3 1 2 强隐蔽集【2 3 】给定一个命题逻辑公式f ，b v a r ( f ) 是一个非空变量子集， 如果b 中变量的任一真值指派f 都能使得f r 】在多项式时间内可解，那么变量集合b 就是强隐蔽集。 定义3 1 3 弱隐蔽集1 2 3 1 给定一个命题逻辑公式f ，b v a r ( f ) 是一个非空变量子集， 如果曰中变量存在一个真值指派f 使得f i r 在多项式内可解且可满足，那么变量集合曰 就是弱隐蔽集。 定义3 1 4 删除隐蔽集【2 l 】给定一个命题逻辑公式f ，b v a r ( f ) 是一个非空变量子 集，如果简化公式f 一召可在多