（计算机应用技术专业论文）基于扩展规则的＃sat近似求解器的研究.pdf

摘要 智能规划是2 0 世纪5 0 年代后期迅速发展起来的一个前沿研究领域，近年来对该领 域的研究取得了革命性的进展。其中，把规划问题编译为s a = r 问题，然后利用高效的 s a t 求解器进行求解的方法是目前规划求解的主流方法之一。研究表明，这种间接求解 有时比直接求解更方便更快捷。撑s a = r 问题是由s a t 问题引出的更具有挑战性的问题， 许多概率推理问题如置信度分析、贝叶斯网络推理、概率规划问题等都可以转化成劳s a t 问题进行求解。这是因为j | j s a t 问题是押完全问题的原型，几乎所有的卯完全问题都能 在多项式时间内归约为j | j s a t 问题。因此，研究撑s a = r 求解技术不仅对规划领域而且对其 他许多领域有着重要的理论价值和现实意义。 许多群s a t 求解器都利用了归结方法，扩展规则方法是一种与归结方法对称的s a t 求解方法，目前该方法已被进一步推广到样s a t 问题求解中，但是它的时间复杂度是指 数级的，效率比较低。 本文在扩展规则的基础上提出了两种撑s a t 问题的近似求解算法：上下界近似 ( u p _ d o 啪a p p r o x ) 和采样近似( s 锄p l e a 聊i r o x ) 。上下界近似是从计算不可满足赋值的 近似个数出发，最终计算出近似模型个数。其基本思想是：对于容斥原理，将每个累加 和视为一项，它的前奇数项之和是一个上界，前偶数项之和是一个下界，文中分析了在 什么情况下能使某个上界或下界与精确不可满足赋值个数的近似偏量在某个范围内( 如 9 0 1 或更小) ，这样可以将该上界或下界视为不可满足赋值个数的近似值，从而得出近 似模型个数。采样近似是将采样方法与改进的扩展规则方法m c r 相结合来得到近似模 型个数。其基本思想是：首先选择若干个变量并赋值，这样可以限定一个子空间，然后 利用采样方法计算出总的模型个数与被限定子空间的模型个数的近似倍率，并利用 m c i e r 计算出被限定子空间的模型个数，将近似倍率乘以被限定子空间的模型个数就可 以得到近似模型个数。 根据以上两种算法，本文设计了两个撑s a t 近似求解器：切) a p p 和s a m a p p ，为了与 精确求解器进行比较，我们实现了精确模型计数算法m c e r 。实验结果表明两种近似求 解器都比精确求解器m c e r 快，其中s a m a p p 的运行速度有了成倍的提高；在精确性方 面，如果近似偏量足够小，u d a p p 能得到与精确值非常接近的近似模型个数，s 觚u 伽 能够得到与精确值比较接近的近似模型个数。 关键词：智能规划；命题可满足性问题；模型计数问题；扩展规则 a b s 仃a c t a n i f i c i a lp l 锄i l i n gi sa 舶n t a lr 舔e a r c hd o m a i l lw l l i c hh 弱b e e l ld e 、r e l o p i n gr 印i d l y 舶m l a t e1 9 5 0 s u pt 0 廿l ep r 懿e n t ，i t sr e s e 鲫c hh 舔c o m e l r o u g l lm o r e l 觚h a l f o fc e n t u 锄d 咖e dr e c e i l u yr e v 0 1 u t i o n a r yd e v d o p m e n t t h ea p p r o a c ho fc o m p i l i i 玛p 1 孤m i i l gp r o b l e mt 0 s a tp r o b l e 芏1 1 ，m 肌而l i z i n g1 l i 曲e 伍c i 饥ts a t h 惯t 0 瑚o l v ei t i so n eo fm em 咖 a p p r o a c h 懿s o l v i n gp l 甜m i n gp b l e m r 销黝f c h 嚣i n d i c a t o dn l a t 廿l ei l l d i r e c ta p p r o a i h e x e c u t e dm o r er a p i d l ym 觚d 慨t 印p r o a c h 群s a rp r o b l e mi sam o r cc h a l l c n g c dp r o b l e m c a u s e db ys a t p r o b l e i n m a n yp r o b a b i l i s t i ci i l 衙衄c cp r o b l e i i l s ，s u c l l 嬲趴a l y s i so fd e 铲e eo f b e l i e i 1 1 f 打朗c eo fb a y e s i 龇n e t v 旧d ( s ，咖b a b i l i s t i cp l a n 面唱p r o b l e m ，a l lm a yb e 仃a i l s l a t e d i n 幻撑s a tp r o b l e m ，a n dr 鼯o l v c db y 撑s a t l v 既撑s a tp r o b l e mi sm ep r o t o t ) ，p eo f 撑p c o m p l e t ep r o b l 锄s n e r e f o r e ，a 1 1 1 1 0 s ta n 卯啪m p l c t cp r o b l 锄s 啪同u c et 0 存s a t p r o b l 锄i i lp 0 1 y n o 面a lt i i c o n s 哪l 肌t l mr e s e 缸c b i n gm er e s o l v e dt 础i i l i q u e so f 群s a th 舔 i n 印o r 觚n l e 0 巧v a l u e 觚da p p l i c 撕o ns i g i l i f i c a n c et 0n o to l l l yp l 瓤m i i 培d o m a i nb u ta l s o o t l l e rd o m a i l 坞 a t 雕吼l i l a q 桴s a ts o l v 哪a r eb 嬲e d0 nr e s o l u t i o n 皿n c i p l e e x t e n s i o nr u l ei sas a t s 0 l 诎略m 锄o d 杜c hs y n m e 臼乜豁也er e s o m o n f l 】n h e r r n o r e i tw 勰删c d t 0s o l v e 样s a tp r o b l e m h o w e v l et i m ec o m p l e x i t yi se x p o n e 血a l ，t l l ee 伍c i c i l c yi sl o w h lt 1 1 i sp 印e r ，w ep r o p o s e 钿ma p p r o 】【i m a t em o d e l 训r 培a l g o r i t h m sb 勰e d0 n e x t 口塔i o nr i l l e ：u p - d 0 、张b 叫i l d 雄，p r o x i m a d o n ( u p d o w i l a p p r o x ) 锄ds a m p l e 雄 p r o x i m a t i o n ( s 锄叩l e a p p r 0 x ) u p d o w 刖蛔x6 r s t l yc 0 u n t st l l ea p p r o x i m a t em 肋b e ro fn os a t i s f a c t o 巧 硒s i 朗m t st l l 饥c o m t sm ea p p r o x i i i l a t en 咖曲e ro f m o d e l s i t sm a i l li d e ai s 鹊f o l l o w i fw e 、，i e wc v e 巧c o m e c u t i v ea d ds 啪o fm ei i l c l u s i o n - e x c l l l s i o np r i n c i p l e 鹬趾i t e i n ，m 既t l l es u m o f 纳n to d di t 觚坞i s 矩u pb o u 咄觚dm e 锄no f 舶n te 啪i t e n l si sad o w nb o u n d w e a r l a l y s et l l a t1 1 r l d 盯w l l a tc o n d i t i o nm e 叩i p r 0 】【i m a t ed i s p e 塔i o no fs o m eu po rd o w nb o u i l d 锄d t 1 1 e 孤顽l r a 伧m m l b e ro f s a t i s f 敷舾r y 勰s i 妒锄t si si nar a n g e 瘩g ) 0 1o rs m a l l e r ) ，s om e u po rd o w nb o u n dm a y b ev i e w e d 嬲m e 印p r o 蛐舢m b 盯o f n 0s 撕s 胁。巧弱s i 印m 锄， t l l e nw ec a nc o u n tt l l ea p p x i m a t em m l b 盱o fm o d e l s s 锄p l 刮巾p xc o m b i i l 骼t h es 卸叩l e a p p r o a c ha n dm ei i l l p r 0 v e da l g o r i n l i no fe x c h i o nr u l em c r t 0a c l l i e v e l ea p p r o x i m a t e n ：u i 】曲e ro fm o d e l s i t sm a i ni d e ai sf o l l o 、i n g a t6 r s t ，w ec ：h o o s es e v e r a lv 撕a b l 镐觚da s s i 弘 v d u et o l e m l i k et i l i s ，w ec a i ir e s t r i c tas u b s p a c e t h e l lu s et h es 锄p l ea p p r o a c l lt 0c o u n t n l e 印p r o x i i i l a 把m u l “p l i e ro ft h et o 协lm m l b e ro fm o d e l s 觚dt h em m l b e ro fm o d d so ft h e f e s t f i 曲e ds u b s p a c e ，跹du t i l i z em c i e rt 0g e tt h en 瑚曲e ro f l n o d e l so f 廿l er e s t r i 鼬e ds u b s p a c e f 1 1 r m e 加1 0 r e ，t l l er e s u l to fm u l t i p l y i n gn l e 印p r o x i i i l a t em u l t 岫l i e rw i m m em m l b e ro fm o d e l s o fm er e s t r i c t e d 鲫b s p a c ei st l l ea p l p r o x i i n a t en 硼曲e ro f m o d e l s n w bd e s i 盟伽。撑s a t 印p r o x i m a t es o l v e r sa c i c o r d 崦t ot w 0a l g o r i t l i m sa b o v e ：u d a p p a n ds a i 】 蛳，a 1 1 d 础1 i e v et h ea l 鲥m mo fa c c u 【r a t em o d e lc o 训i 培m c e rf o rc o m p 啦n l e 铆oa p p r o x i i i l a t es o l v e r s 、i ma 0 鼬s o l v 既e x p 舐m 饥t 谳l t si n d i c a t e dm a tt l l e 铆。 印p r o x i m a t es 0 1 v e 墙e x e c u t e dm o r er a p i d l yn l a i ia c l c 哪兆s o l v e fm c e r w h e r e s 锄螂p h 瑟 m u l t i p l ei i i u r 0 v 锄e n t n l er 衄_ i l i n gs p e e d 1 1 1t l l ea c c u r a c y u d a p p c a i l g a i l l 玲 a p p r o x i m a t em m l b e ro fm o d e l sw 1 1 i c ：hi sv e 巧n e a rt 0 l ea c 砚l r a t ev a l u ei fm ea p l p y r o x i m a t e d i s p e r s i o ni sa d 删e s m a l l a n dsa i 】咖c a ng 血m ea p p r o x i m a t em m l b e ro fm o d d s 、) v _ m 6 h i sr e l 撕v e l vc l o s et 0t h ea c ( 撇t ev m u e k e yw o r d s ：加- t i f i c i a lp l 锄n i i l g ；p r o p o s i 廿o ns a t i s 缸舶r yp r d b l e m ；m o d e lc o u n t i n gp 暂0 b l e m ； e x 钯啮i o nr u l e m 独创性声明 本人郑重声明：所提交的学位论文是本人在导师指导下独立进行研究工作所取得 的成果。据我所知，除了特别加以标注和致谢的地方外，论文中不包含其他人已经发 表或撰写过的研究成果。对本人的研究做出重要贡献的个人和集体，均已在文中作了 明确的说明。本声明的法律结果由本人承担。 学位论文作者签名：量垒整日期： s o l i 口s 学位论文使用授权书 本学位论文作者完全了解东北师范大学有关保留、使用学位论文的规定，即：东 北师范大学有权保留并向国家有关部门或机构送交学位论文的复印件和电子版，允许 论文被查阅和借阅。本人授权东北师范大学可以采用影印、缩印或其它复制手段保存、 汇编本学位论文。同意将本学位论文收录到中国优秀博硕士学位论文全文数据库 ( 中国学术期刊( 光盘版) 电子杂志社) 、中国学位论文全文数据库( 中国科学技 术信息研究所) 等数据库中，并以电子出版物形式出版发行和提供信息服务。 ( 保密的学位论文在解密后适用本授权书) 学位论文作者签名：至垒整 日 期：坐堕：! ：! 学位论文作者毕业后去向： 工作单位： 通讯地址： 指导教师签名： 日期： 带仪 、 例、口良 电话： 邮编： 东北师范大学硕士学位论文 第一章引言 1 1 研究背景 智能规划是人工智能中较早的研究领域之一，并且逐渐成为一个研究热点。基于 s a = r 的方法是规划求解的主流方法之一，1 9 9 2 年蛋洳t z 等第一次把规划问题求解转化为 命题可满足性问题( s a t 问题) 【l 】，这种方法使得s a t 求解的新技术可以直接应用于规 划系统，从而有效地推动了规划研究。在国际规划器竞赛中，基于s a t 的规划器表现出 优秀的性能，如b 1 a c k b o x 【筋、s a 皿l a n 0 4 【3 1 、m a x p l 锄【4 】分别获得了第一届、第四届、第 五届s n m s 规划域的冠军。 s a t 问题是命题可满足性问题的简称，是当今计算机科学和人工智能研究的核心问 题。随着对s a t 领域的深入研究，产生了一个非常具有挑战性的问题：模型计数问题 ( m o d c lc 0 硼t 啦，简称为撑s a = i 问题) 。群s a = r 问题需要计算出给定命题公式( q 师范式) 的模型的个数，也就是使命题公式为真的赋值个数，它的复杂性高于命题可满足性问题， 是卯完全的【5 1 。许多概率推理问题，如置信度分析【5 】、贝叶斯网络推理【6 】、概率规划问 题【7 】等，都可转化成模型计数问题进行求解。这是因为s a t 问题是杼完全问题的原型， 几乎所有的杼完全问题都能在多项式时间内归约为撑s a t 问题。因此，研究群s a t 求解 技术不仅对规划领域而且对其他许多领域有着重要的理论价值和现实意义。 目前，许多s a t 求解器都利用了归结方法，扩展规则方法【8 】是一种与归结方法对称 的s a t 求解方法。许多模型计数方法，主要是把s a t 求解方法进一步扩展到栉s a t 求解中。 基于d p l l 【9 】【1 0 】方法是目前命题逻辑中基于归结原理的最快的定理证明方法之一， 在文献【1 1 】中，b h n b a u m 和l 0 刎i 直接扩展d p l l 来求解模型计数问题，提出了模型计 数算法c d p 。在算法c d p 的基础上，b 础和p e h o u s h e k 利用连接图来描述变量之间的 关系，这样可以将公式分成多个子公式来单独求解【1 2 1 。s a n g 等人设计的c a c h e t 系统在 d p u ，方法中混合使用了子旬学习和组件缓存的策蝌1 3 】【1 4 】。然而，所有这些模型计数方 法所花费的时间代价都是指数级别的，并且只能解决相对小的命题公式。因此，s 妇 等人在文献【1 5 】中提出了一种近似的模型计数方法a 卵r o x c o u n t ，它通过采样方法来估计 模型的个数，但是在求解子空间的模型个数时用的还是归结方法。 扩展规则方法是一种与归结方法对称的s a t 求解方法，该方法的主要思想是沿着归 结的逆向求解s a t 问题，并且利用容斥原理解决由此带来的空间复杂性问题，对于一个 命题公式，如果子旬中互补文字较少时，基于归结的方法效率较高；如果子句中互补文 字较多时，基于扩展规则的方法效率较高。2 0 0 7 年，殷明浩和孙吉贵提出了一种基于扩 展规则的模型计数方法m c e r 【1 6 】【1 7 】，该方法首先计算出命题公式的不可满足赋值个数， 然后计算出模型个数。但是，对于一般的子句集而言，利用容斥原理来计算不可满足赋 值个数时需要计算2 n l 项，效率比较低。 1 东北师范大学硕士学位论文 1 2 本文的主要工作 1 在扩展规则方法的基础上提出了两种模型计数近似求解算法：上下界近似和采样 近似。首先给出了近似偏量的定义，然后具体设计了这两种算法。 ( 1 ) 上下界近似首先计算出不可满足赋值的近似个数，然后计算出近似模型个数。 其基本思想是：对于容斥原理，将每个累加和视为一项，它的前奇数项之和是一个上界， 前偶数项之和是一个下界。因此，考虑在什么条件下，能将某个上界或下界作为其近似 值。文中具体分析了在什么情况下能使某个上界或下界与精确不可满足赋值个数的近似 偏量在某个范围内，这样可以将该上界或下界视为不可满足赋值个数的近似值，从而得 出近似模型个数。 ( 2 ) 采样近似是将采样方法与改进的扩展规则方法相结合来得到近似模型个数。 其基本思想是：首先选择若干个变量并赋值，这样可以限定一个子空间，然后利用采样 方法计算出总的模型个数与被限定子空间的模型个数的近似倍率拖坳胁，并利用改进 的扩展规则算法计算出被限定子空间的模型个数s 。，将胁坳胁乘以s 。就可以得到近 似模型个数。 2 根据以上两种算法设计了两个撑s a t 近似求解器：u d a p p 和s a m a p p ，并实现了精 确模型计数算法m c e r 。实验结果表明两种近似求解器都比精确求解器m c e r 快。如果 近似偏量足够小，u d a p p 能得到与精确值非常接近的近似模型个数，但是需要花费更多 的时间，而s 觚却p 能够在很短的时间内得到与精确值比较接近的近似模型个数。 1 3 论文的结构 第一章介绍了本文的研究背景、主要工作及论文结构。 第二章首先介绍了规划的主要求解方法，然后介绍了几种基于可满足性的规划方 法，以及该类规划器在国际规划器竞赛中的表现。 第三章介绍了命题可满足性问题和模型计数问题及其它们的求解方法。 第四章首先回顾了扩展规则的定义及其相关定理，以及基于扩展规则的撑s a t 求解 方法m c e r ，然后提出了两种基于扩展规则的烬a 1 近似求解方法：上下界近似和采样 近似，并将它们与a 唧x c 0 u n t 进行了比较。 第五章根据提出的两种算法，设计了两个撑s a t 近似求解器：u d a p p 和s a m a p p ， 并进行实验测试以及结果分析。 第六章对全文进行总结，并指出将来要做的工作。 2 东北师范大学硕士学位论文 第二章基于可满足性的规划 智能规划理论是2 0 世纪5 0 年代后期迅速发展起来的一个前沿研究领域，至今它的 研究已达半个世纪之久，其发展对计算机科学、人工智能、认知科学等领域产生了重要 的影响，并广泛应用于机器人、自然语言理解、知识推理、人机交互、游戏角色设计等 方面。 把规划问题编译成s a = r 问题，然后利用高效的s a t 求解器进行求解的方法是目前 解决规划问题的主流方法之一。这里有必要先介绍规划的主要求解方法，然后详细介绍 基于可满足性的规划。 2 1 规划主要求解方法 智能规划是根据给定的对象、操作、初始条件和目标，找到能从初始条件到达目标 的一系列动作，这一动作序列就称为规划。虽然研究人员自从人工智能的早期就开始研 究规划，但近年来该领域才取得革命性的发展，这主要来源于规划领域的三种新方法。 第一种方法是1 9 9 2 年l n z 等把规划问题转化为命题可满足性问题，这种方法使得命 题推理系统中的新技术可以直接应用于规划系统，从而有效地推动了规划研究；第二种 方法是1 9 9 5 年由b l u m 和f l 璐t 提出的图规划【1 8 】【1 9 1 ，这种方法第一次采用图的方式来解 决规划问题，开辟了规划求解的新途径；第三种方法是1 9 9 8 年由b o i l e t 和g e 伍财提出 的启发式方法【冽，它利用启发式函数来指导状态空间搜索，表现出很强的问题求解能力。 基于这三种方法的规划器在两年一度的国际规划器竞赛中屡获冠军，表现出优异的性 能，本文只介绍第一种方法。 2 2 基于可满足性的规划( p l 猢i n ga ss a t i s f i a b i l i t y ) 把规划问题编译成命题公式，然后利用高效的s a = r 求解器进行求解的方法是目前规 划求解的主流方法之一。一个简单而有代表性的例子是b l a c k b o x 规划裂2 1 ，仅需6 分钟就能从1 0 1 6 可能状态中发现一个含1 0 5 个动作的逻辑规划。而且命题规划的研究己 成功应用于美国航空与航天局( n a s a ) 的d e 印s p a c eo n e 宇宙飞船自动控制器。 2 2 1 基于可满足性的规划方法 1 9 9 2 年，龇和s e l i i l 锄首次提出了一种被称为“线性编码的基于定理机器证明的 规划问题的表示方式，将经典的规划问题转换为命题可满足性问题进行求解。该编码中 的公理主要由表示初始状态和目标条件的公理、操作蕴涵前提和效果的公理、操作互斥 公理和经典框架公理等组成。线性编码第一次给出了如何将经典规划问题转换为命题可 3 东北师范大学硕士学位论文 满足性问题的方法，进而提出了一种新的规划方法一基于可满足性的规划方法。但是， 该编码固有限制了在一个时间步仅有一个动作发生，这使得其处理能力有限，只能处理 生成顺序规划解的情况，而不能处理包含并发规划解的情况。 基于s a t 的规划问题的形式化模型，可以更加精确的反映基于各种约束的现代规划 系统的理论框架。在基于可满足性的规划方法中，一个模型对应于对系统中的原子命题 的一种真值指派。一个规划问题对应于一个公理集，使得满足该公理集的任意有效模型， 都对应于一个有效的规划解。 该方法的缺点是不能处理需要并发规划解的规划问题，尤其适合于b 1 0 c k sw 0 r l d 这 样的动作只能顺序执行的问题，而对于后勤域等基于调度的规划问题，无法通过在某些 时间点并发执行几个不相关动作得到最小时间步的规划解。 2 2 2 基于可满足性的规划系统s a t p l a n 1 9 9 6 年，舭等提出了一种新的编码方式：基于状态的编码，并设计了s a l t l a n 规划系绀2 1 1 ，第一次将基于可满足性的规划思想设计成成型的系统。 基于状态的编码采用公理来断言单一状态的有效性和表示操作，并采用了状态转移 公理( 即解释性框架公理) 来替换经典框架公理，它是用来表示状态之间的转移，其中 每个转移可以是应用任意数目个互相不冲突动作的结果。添加公理断言动作需要它的前 提和效果，冲突的动作是互斥的等等。 s a t p u 州的输入为规划问题对应的公理公式集合，需要手工的将该表示形式转换 为基于状态的中间编码，输出为要得到的规划解。其成功之处在于其逻辑表示和强大的 通用推理算法( 例如眦a t 四】) 。 规划问题的基于状态的编码对应的解为一个状态序列。这个状态序列中状态的转换 对应了规划解中的动作执行。 同年，舭h ，m 锄l e s t e rd 和s e h n 觚b 提出了提升的因果编码【2 3 1 。该编码包含两 部分内容：将规划问题转换为提升的因果编码，和将提升的因果编码还原为标准s a t 的 编码。该规划方法首先将规划问题转换为对应的提升的因果编码，之后将提升的s a t 表 示通过添加原子公式上的等价关系归约为标准的s a t 表示，调用s a t 求解器进行求解。 同时，其提出了通过删除状态变量和动作变量，进一步约简变量数目的思想，这在很大 程度上压缩了编码空间。 1 9 9 7 年，e n l s tm ，m i l l s t e i i ltd 和w r e l dds 设计出了第一个基于s a t 的自动规划器 m e d i c 【2 4 1 ，可以自动地将问题编码和提取规划解。 2 2 3 基于可满足性的规划系统b i a c k b o x 1 9 9 8 年，i a u t z 和s e l m m 设计了倍受关注的b 1 a c k b o x 规划系统，该规划器基于s a l t 框架和规划图方法。 基于图规划的编码，利用了图规划中的规划图构建方法，其原理是：首先构建一个 时间步为力的规划图，并将该规划图自动转换为c n f 公式( 从目标层开始反向执行转换 4 东北师范大学硕士学位论文 过程) ，调用s a t 求解器进行可满足性判定，如果判定为可满足，则找到了规划解对应的 模型，进而还原为相应的规划解，否则继续构建时间步为刀+ l 的规划图。与线性编码相 比，基于规划图的编码添加了后向链公理，省略了操作蕴涵效果公理和框架公理。 b l a c k b o x 首先将s 己p s 型规划问题转换为s a t 问题，并使用快速的s a l 求解器 进行有效的求解，之后将找到的模型转换为相应的规划解。规划算法中采用了随机的局 部搜索s a t 求解器w 批艇t 和两个完备的s a t 求解器s a t z 【2 5 】和r e ls “2 6 】对s a t 问题进 行求解，之后的版本采用了当时最先进的s a t 求解器z c h a 一2 7 】【2 8 1 及其改进版本 j e n l s “2 9 1 。 2 2 4 该类规划器在国际规划器竞赛中的表现 b 1 a c k b o x 参加了1 9 9 8 年举办的第一届国际规划竞赛( h l t 删o n a lp l 锄钉 c o m p 甜t i o n ，碑c ) ，并获得了s t r 口s 问题域的冠军，但是在2 0 0 0 年的第二届国际规 划竞赛中成绩很不理想。 2 0 0 4 年，改进的s 鼬曙u 阑参加了第四届m c ，并获得了s t i m s 规划域叫j m a l p 1 锄i l i n g 组的冠军。结果显示，s a t p u 蝌0 4 的优势明显，在5 个域获得了第一，2 个域获 得了第二，其他的参赛规划器最好的是4 个域获得了第二。s a t p u 蝌的再一次成功主要 取决于s a t p u 斟0 4 中采用了最先进的s a t 求解器s i e g e 【3 0 】。s a r p u 蝌0 4 的成功，使得基 于可满足性的规划研究再一次被广泛关注。这至少可以说明：在最优s n 己口s 规划域，完 全依赖于s a t 求解效率的基于可满足性的规划方法还是有一定优势的。 2 0 0 6 年，z h x i n g 和c h e n x i l l 等在s a t p l 气n 0 4 的基础上重新做了改进，设计出了 能够处理时态规划问题的规划器m a ) 【p l 强，其中的s a t 求解器采用了z c h 碉围铂p e r t 。进 一步表明：基于可满足性的规划方法对于时序规划问题，同样有很强的表示和处理能力。 龇等人设计的s 筒【p l a n 0 6 【3 l 】是在b l a c k b o x 规划器上的又一次改进。它和 s a t p l a n 0 4 采用了相同的s a t 求解器，二者最主要的区别在于在规划图生成过程中是否 计算互斥传播。s 触r p l a n 0 4 由于存储的限制，没有计算互斥传播，而s a r p u 蝌0 6 中生 成了命题变元之间的互斥子句，没有生成动作变元之间的互斥子句。 m a x p l 纽和s a t p l ，a n 0 6 均参加了2 0 0 6 年第五届口c ，并列获得了s t i t m s 规划域 o p 廿i i l a lp l a n n i n g 组的冠军。 5 东北师范大学硕士学位论文 第三章命题可满足性问题的扩展一模型计数问题 模型计数问题是由命题可满足性问题引出的一个非常具有挑战性的问题，它的复杂 性高于命题可满足性问题，是撑p 完全的，而且许多模型计数方法都是s a t 求解方法的 进一步推广。这里有必要先简单了解s a = i 问题及其求解技术，然后介绍j | s a t 问题及已 有的求解方法。 3 1 命题可满足性问题 s a t 问题是命题可满足性问题的简称，它是当今计算机科学和人工智能研究的核心 问题，也是计算机科学技术发展的“瓶颈，许多问题如程控电话的自动交换、大型数 据库的维护、大规模集成电路的自动布线、软件自动开发、机器人动作规划等，都可转 化成s a t 问题【3 2 1 。这是因为s a t 问题是n p 完全问题的原型，几乎所有n p 完全问题都 可以在多项式时间内归约到s a = r 问题。研究表明，许多n p 完全问题转化成s a = i 问题 进行求解都比直接求解更方便更快捷。 原子或原子的否定称为文字，原子有时也叫作变量，它的取值为m e 或忍舭；一 个子句是有限个文字的析取；一个c n f 范式是有限个子句的合取，有时也叫作子句集。 对于一个给定的命题公式( q 师范式) ，s a t 问题就是判断是否存在一组变量的赋值使 得给定的公式为真。如果存在，则称该公式是可满足的，这组赋值称为可满足赋值，也 就是一个模型；否则，称该公式是不可满足的。 3 2s a t 问题的求解方法 s a t 算法包括完备( c o m p l e t e ) 算法和非完备( m c o m p l e t e ) 算法两大类【3 3 1 。完备 算法可以保证在运行完毕以后，要么至少找到一个可满足赋值，要么证明可满足赋值不 存在，即证明公式的不可满足性。非完备算法不能保证最终或者返回一个可满足赋值， 或者证明给定公式是不可满足的。 完备算法主要分为基于衍生的和基于分支回溯的两大类，这两种方法都属于归结方 法。文献 8 中林海和孙吉贵等人提出了一种与归结方法对称的s a t 求解方法扩展规 则方法。该方法的主要思想是沿着归结的逆向求解s a t 问题并且借助容斥原理解决由 此带来的空间复杂性问题，这里只介绍基于归结的完备算法，扩展规则算法将在下一章 介绍。 基于衍生的完备算法的基本思想是不断地由两个子句产生一个衍生子句，一直进行 下去，如果产生了空子句，就证明了公式是不可满足的，而如果无法产生新的衍生子句 了，就证明公式是可满足的。由于这类算法会导致计算空间的指数爆炸，因此从上个世 6 东北师范大学硕士学位论文 纪8 0 年代中期之后没有大的发展。基于分支回溯的算法由d p l l 算法发展而来，其基本 思想是不断地选择分支变量进行赋值并根据赋值利用单元传播( u i l i t p r o p a g a t i o n ) 来简 化实例，在有冲突的情况下回溯到另一分支继续搜索。这一类算法虽然最坏情况下时间 复杂性仍然是指数的，但在实际应用中取得了很大的成功。许多高效的完备算法几乎都 属于这一类算法，如g l l a s p ，p o s i t 【3 5 1 ，s a t o 【3 6 】，r c ls a t ，c l l a 纸 非完备算法是在运行过程中试图找到一个可满足的赋值，如果找到则证明公式是可 满足的；如果到达规定的时间还不能找到，不能说明公式是不可满足的。非完备算法的 一种思想是随机局部搜索( 如g s a 一3 7 1 ，w a l k s a t ) ：首先随机给一组赋值，将不满足的 子句数目看成优化目标，在赋值空间中随机搜索。另一种方法是s p ( s 删p r o p a g a t i o n ) 算法【3 8 】【3 9 】，它将统计物理学方法应用于s a t 问题的求解中。s p 算法可以看作是一种基 于d p l l 的回退搜索算法，它首先计算一组满足变量赋值的概率边缘分布，并逐步确定 具有最大分布值的变量。s p 算法在计算边缘分布的过程中，采用一种消息传递技术， 并利用调查迭代函数反复地计算传递的消息。一旦传递的消息收敛，就利用启发式消解 过程找到发生“冻结的变量，并利用这些“冻结 的变量逐步简化布尔公式。令人惊 奇的是，s p 算法几乎很少回退，换言之，s p 算法在启发式引导中大多数情况下都是高 效的。非完备算法在很多类别的可满足实例上得到了有效的运用，在有些实例上其性能 远远优于完备算法。但是对于验证实例的不可满足性，到目前为止只有完备算法是实用 有效的。 3 3 模型计数问题 随着对s a t 领域的深入研究，产生了一个非常具有挑战性的问题：模型计数问题 ( 撑s a t 问题) 。魑a t 问题需要计算出给定命题公式的模型的个数，也就是使命题公式 为真的赋值个数。它的复杂性高于命题可满足性问题，是卯完全的。许多概率推理问 题，如置信度分析、贝叶斯网络推理、概率规划问题等，都可转化成模型计数问题。这 是因为群s a ：r 问题是卯完全问题的原型，几乎所有的稃p 完全问题都能在多项式时间内归 约为 s a t 问题。因此，研究舟s a t 求解技术不仅对规划领域而且对其他许多领域有着重 要的理论价值和现实意义。 3 4 撑s a = r 问题的求解方法 3 4 1 精确求解方法 目前，存在许多精确模型计数方法。基于d p l i ，方法是目前命题逻辑中基于归结原 理的最快的定理证明方法之一。 在文献【1 1 】中，b i n l b a u m 和l 0 z i n s l 【i i 证明只要子问题不含不可满足子句，可以直接 扩展d p l l 方法来求解模型计数问题，并提出了基于d p l l 的模型计数算法c d p 。c d p 的 主要思想如下：设肘( 习表示给定公式集合的模型个数，由于子公式人口和 吲的 7 东北师范大学硕士学位论文 模型交集为空，所以 m ( ) = m ( 口) + m ( 1 口) 利用单元传播对子公式进行化简，这样，出现在中的变量有可能不出现在化简后的子 公式中。若中有行个变量，其中化简后的子公式 口和 吲中分别有刀j 和刀2 个变量出 现，则 m ( ) = 必( 跏f 勿仰( z 口) ) 幸2 肛啊+ m ( 踟印唧( 1 口) ) 幸2 露- 也 在算法c d p 的基础上，b 啦和p e h o u s h e k 设计了r - e l s a t 系统。它通过连接图来描述 变量之间的关系：连接图的节点为出现在公式集合中的变量，如果两个变量出现在同一 子句中，那么代表这两个变量的节点之间就存在一条边。通过这种方式可以将中的所 有变量分成多个不相连的组件，从而将分成子公式，：，；，每个子公式都 代表着连接图中独立的部分来单独求解，则 ， 膨( 劲= i l 膨( z ，) 筲 s a n g 等人设计的c a c h e t 系统在d p l l 中混合使用了组件缓存和子旬学习的策略。组件 缓存记录了已经计算的子公式，这样可以避免重复计算：子句学习则是通过分析出现冲 突的原因得到学习子句，将学习子旬加入原公式来避免遇到相同的冲突。 d a r 耐c h e 等人提出可以通过知识编译的方法来求解模型计数问题4 0 4 2 】。将给定命题 公式转换为d n n f 范式后，可以在多项式过程内求解模型计数问题。无论在知识编译阶 段还是在之后的求解阶段，该方法都是基于归结原理的。 扩展规则方法是一种与归结方法对称的s a t 求解方法，该方法的主要思想是沿着归 结的逆向求解s a t 问题并且借助容斥原理解决由此带来的空间复杂性问题，对于一个命 题公式，如果子句中互补文字较少时，基于归结的方法效率较高；如果子句中互补文字 较多时，基于扩展规则的方法效率较高。殷明浩和孙吉贵提出了一种基于扩展规则的模 型计数方法m c e r ，它可以看作是基于归结原理的模型计数方法的一种补方法。该方法 不是直接计算所有可满足赋值个数，而是先计算出命题公式的不可满足赋值个数，然后 计算出模型个数。 3 4 2 近似求解方法 以上所有精确模型计数方法所花费的时间代价都是指数级别的，并且只能解决相对 小的命题公式。因此，s e l m a n 等人在文献【1 5 】中提出了一种近似的模型计数方法 蛳x c 伽咀t ，该方法通过采样来估计模型的个数。基本思想是：首先利用采样方法 ( s 觚l p l e s 3 1 ) 从子句集的解空间中得到k 个样本，每个样本是使满足的一个赋值。 在这k 个样本中，考虑中的一个变量而，而为m e 的样本个数记为群( 而= 胁p ) ，而为 忍豇p 的样本个数记为群“= 凡西力。假设尺个样本是从均匀分布的模型中采样得到的， 并且尺足够大，那么 8 东北师范大学硕士学位论文 丝g 仝型垫! 三丝生 肘( ) k 丝! 兰全! 1 2 堂生! 三丝丝! m ( ) k m ( ) 表示输入公式的模型个数。若而的赋值为m p ，则 m ( ) 南彤( 卧而) 类似地，可以将 而视为，递归地继续进行下去。利用采样方法的一个优点是通过 调节样本空间的大小能够很好地控制运行时间，它依赖于我们需要的近似模型个数的精 确程度。进一步，他们对该方法进行了优化，使最后得到的近似模型个数更接近于精确 模型个数m 】【4 5 1 。但是求解子空间的模型个数时用的还是归结方法。 9 东北师范大学硕士学位论文 第四章基于扩展规则的j i s a t 近似求解方法 本文是在扩展规则的基础上提出了两种s a t 近似求解方法，为了讨论方便，首先 介绍本文需要的一些背景知识。 这里对一些符号进行约定：用，z ：，表示q 师范式，有时也看作子句集； 用c ，c l ，g ，表示单个的子旬，有时也把子句理解成文字集合的形式；通常，材表 示一个子句集中所有原子的集合，有时也将原子当成变量。 4 1 扩展规则及其相关定理 首先引入扩展规则网，它是本文其它工作的基础。扩展规则定义如下： 定义4 1 给定一个子句c 和一个原子的集合m ： d = cv 口，cv 吲i 口m 并且口和，口都不在c 中出现) 把从c 到d 中元素的推导过程叫做扩展规则，d 中的元素叫做应用扩展规则的结果。 例如，给定子旬口v 南和原子集合m = 红，6 ，c ，对子句口v 南应用扩展规则的结果 为口v 1 6v c ，口v 山v l c 。下面来看一下子句c 和它扩展之后的结果d 之间的关系。 定理4 1 子旬c 和它扩展后的结果d 是等价的。 这样，我们可以对子句集中的子句应用扩展规则。定理4 1 保证了应用扩展规则后 的子旬集和原子句集等价。因此扩展规则可以被看作是一条推理规则。 定义4 2 一个非重言式子旬是集合m 上的极大项当且仅当它包含集合肘上的所有原子 或其否定。 例如，给定原子集合m = 函，6 ，c ，d ，口v 山v cv d ，口v 南v 呷v d 是m 上的极大项， 4v 而v c 则不然。 定理4 2 给定一个子句集，其中所有原子的集合是m ( i 矧= m ) ，若中的子句都是 m 上的极大项，则子句集不可满足当且仅当中含有2 ”个互不相同的子句。 事实上，定理4 2 是基于扩展规则方法求解命题可满足性问题的核心思想。注意如下 事实：对于一个子句集而言，如果其中的子句都只含有一个相同的原子，那么它不可满 足当且仅当它是函，口 的形式，即含有2 个子句；如果其中的子旬都含有两个相同的原 子，那么它不可满足当且仅当它是矗v6 ，口v ，6 ，卅v6 ，1 口v ，6 的形式，即含有4 个子句， 以此类