（计算机软件与理论专业论文）基于扩展规则的＃qbf求解系统的研究及实现.pdf

摘要 智能规划是设计某个( 组) 实体从初始状态出发，到达目标状态的动作序列，其结 果被称为规划解。目前的规划求解器只能求解问题的个解，不能求解问题的所有解的 个数，如对手规划，二人游戏赢的所有策略数等问题。虽然这些智能规划问题可以通过 相应的处理器( b 1 a c k b o x ) 转化成存q b f 阎题进行求解，但是目前还没有开发出鼻q b f 求 解器。 针对这一问题，本文提出了一类新的求解聋q b f 问题的方法一基于扩展规则的 群q b f 计数方法，用来求解相应的智能规划问题。这类方法的基本思想是利用扩展规则 把原公式扩展成和它等价的极大项组成的集合，然后利用极大项的个数来进行撑q b f 计 数，并利用容斥原理来解决空间复杂性问题。这类方法与基于归结的方法相比，当包含 互补文字的子旬越多时效率越高，因此它们可以看作是和归结互补的方法。基于此思想， 本文首先提出了一种基本的基于扩展规则的 6 l q b f 计数方法；然后，为了提高效率，本 文还提出了一种改进的# q b f 计数方法，即基于知识编译的方法，其思想是把要求解的 问题应用扩展规则编译成殁) c c i l 语言，然后进行i q b f 计数：最后，受组件分析思想 的启发，本文提出了基于组件分析的拌q b f 计数方法，这种方法的思想是把要求解的问 题先分解成组件，然后对每个组件利用扩展规则进行求解。由于该方法中还加入了单文 字处理的功能，所以与前两种方法相比，它不仅可以处理比较一般的拌q b f 计数问题， 还可以处理规模较大的群q b f 计数问题。 ，在给出算法的基础上，本文采用c + 语言对算法进行了实现，设计了基于扩展规则 的三个群q b f 计数系统：斑r 、拌k c e r 和群c s e r ，并用实例对其性能加以测试。实验结 果表明，在处理一般问题时，拌e r 的时间复杂性是指数级的，效率比较低：群k c e r 算 法理论上要优于拌e r 算法，但是经过编译后的子句集扩大的规模在最坏情况下是指数级 的，所以它的效果也不尽如人意；拌c s e r 算法由于加入了单文字处理和组件分析的功能， 使得它处理阎题的能力比前两种方法要好。由于日前国内尚没有个公开成型的基于扩 展规则的# q b f 计数器，所以本文的三个系统特别是撑c s e r 系统将具有一定的研究价值 与应用前景。 关键词：群q b f ；扩展规则；知识编译；e p c c l ；组件分析；单文字 a b s t r a c t j n t e l l 追e n c ep l a i l l l i n gi sas e q u e n c e0 fs e t so fa c t i o i l st h a t w i l la c h i e v e 协eg o 砒s0 fa p r o b l e m t l ev a | i ds e q u e n c eo fs e t so fa c t i o n si sc 2 i l l e dp l a n i l i i 培s o l u t i o n a tp r e s e n t ，a 1 1m e p l 锄e r sc a ng e tj u s to n es o l u t i o n ，b u tn o tm en 眦b e r0 fa l l 出es o l u t i o n so f t l l ep r o b l e m ，s u c h 嬲t l l en m b e ro f w 岫gs g i e sa to p p o s i t i m 谢p l a 锄i 1 1 岛恤d l l a l 咎m l e sa i l ds o0 n t h e s e i i l t e l l i g e n c ep 1 锄1 1 i 】 1 9p r o b l e m sc a nb e 衄1 s f 0 】瓶e di i l ：t 0 # q b f 吐l r o u 曲t 1 1 eb l a c k b o 墨b u ti ti s ap i t yt h a 士m e r ei sn o 群q b fc o u n t e rn o w ： t ob e 如e da tt i l e s ep r o b l e i i l s ，n e wa p p r o a c h e so f 捍q b f 哪堍砌c hb a s e do n e x t e i l s i o nr u l ea r ep r o p o s e dt od e a lw i m 也ec o 盯e s p o n d i n gi 1 1 t e l l i g e n c ep l 棚gp r o b l e n l s t h eb a s i ci d e ao ft h e 印p r o a c h e si st 0d e d u c et 1 1 es e to fa l lt l em a 划m 啪t e n i l sf o r 群q b f c o 蚰t i n ga 1 1 dt 0u s et l l ei n c l u s i o n e x c l u s i o np r i n c i p l et oc i r c u m v e n t l ep r o b l e mo fs p a c e c o m p l e x i t y c o m p a r e dw 曲t h er e s o l u t i o n 印p r o a c h e s ，也em o r ec o m p l e m e n ：t a 巧l i t e r a l ( s ) m e c l a u s e sc o n t a 畦出eg r e a t e fe 篮c i e n c y 也ea p p r o a c h e sa r e ，s 0o u ra p p r o a c h e sc a nb es e e na sa c o m p l e m e n t a 一够t 0 吐l er e s o l u t i o na p p r o a c h e s f i r s t l y ，ab a s i ca p p r o a c ht i l a tb a s e do n 廿l e e ) ( t e i l s i o nr u l ei sp r o p o s e dw h o s eb a s i ci d e ai st 1 1 es 锄ea sm ei d e ad e s c r i b e da b o v e s e c o n m y ， t o i n l p r o v e 缸l ee 街c i e n c y ，a 1 1 0 m e ra p p r o a c hm a tb a s e do nk n o w l e d g ec o m p i l 撕o ni s p r o p o s e dt o o t h eb a s i ci d e ai st 0c o m p i l em ep e n d i n gp r o b l e mt oe p c c l ，m e nd o 廿l e 捍q b f c o 眦i i l g t m r d l y ，m ei d e ao fc o m p o n e n t sa i l a l y s i si i l s p 曲e d 仕l el a s t 印p r o 础1 t h eb a s i ci d e a o f 缸l i s 印p r o a c hi st od e c o m p o s e 也ep e n d i n gp r o b l e mi n t oc o m p o n e n t s 锄dt os o l v e 血e i n d i v i d 训c o m p o n e n _ t s ，也e nt om l l l t i p l yt l l em o d e l s0 ft h ei n d i v i d u mc o m p o n e n t st 0g e t 吐l e m o d e l so fn l eq b fp r o b l 锄t h i sa p p r o a c ha l s oh a sa b 啦t od e a j 谢t h 恤s 崦l el i t e r a l s c o m p a r e d 、) l ，i 也m ea n t e i j o r 印p r o a c h e s ，t 1 1 el a s f to n ec a nd e a lw i m m o r em i v e r s a la n dl a 略e r 鼻q b fc o u n t i n gp r o b l e m s b a s e d 锄t l ea l g o r i t h m sp r o p o s e da b o v e ，w e 胁e 趣科e m e n t e d 也r e ei l e w 拌( 冯f c o 嘶i n gs ) ，s t e m s ：拌e r 、姗( c e ra n d # c s e r e ) 叩e r i m e n tp r 0 v e dt h a tm et i m ec o m p l e ) 【i 锣o f 撑e ri se x p o n e n t i a la i l dm ee 街c i e n c yi sl o ww h e ns 0 1 v 崦m eg e n e r a jp r o b l 锄s 拌k c e ri s b e t t e rt h a nm e 拌e ri nt h e o 吼h o w e v e r 此s c a l l eo f m ec l a u s e s 碰e rc o m p i l e di se x p o n e n t i a ji 1 1 吐1 ew 嘣s o 也ee 统c to f 群k c e ri sd i s s a t i s f a c t 0 巧b e c a u s e 捍c s e rh a s 也ea b i l 毋o fs 咄l e l i t e r a lp r o c e s s i i l ga i l dc o m p o n e ma n a l y z i i l g ，i ti sb e t t e r 血a n 也ef o m e rt 、v o 妙g t e m s m o r e o v e r ，a st h e r ei sn or e a d ym o d e lc o 眦t m gs y s t e mb a s e do nt h ee ) 【t e r l s i o nr u l ei r l l a r l d ，s oo u r s y s t e i n s ，e s p e c i 2 l l l y l e 群c s e rw n lb es i 嘶f i c a n tb o m 血r e s e a r c ha n dp r a c t i c e k e yw o r d s ：存q b f ；髓e n s i o nr u l e ；k n o w 】e d g ec o m p i l i n g ；e p c c lc o m p o n e n t a n a l y s i s ；s i n g l el i t e r a l s 独创性声明 本人郑重声明：所提交的学位论文是本人在导师指导下独立进行研究工作所取得 的成果。据我所知，除了特别加以标注和致谢的地方外，论文中不包含其他人已经发 表或撰写过的研究成果。对本人的研究做出重要贡献的个人和集体，均已在文中作了 明确的说明。本声明的法律结果由本人承担。 学位论文作者签名： 学位论文版权使用授权书 本学位论文作者完全了解东北师范大学有关保留、使用学位论文的规定，即：东 北师范大学有权保留并向国家有关部门或机构送交学位论文的复印件和电子版，允许 论文被查阅和借阅。本人授权东北师范大学可以采用影印、缩印或其它复制手段保存、 汇编本学位论文。同意将本学位论文收录到中国优秀博硕士学位论文全文数据库 ( 中国学术期刊( 光盘版) 电子杂志社) 、中国学位论文全文数据库( 中国科学技术 信息研究所) 等数据库中，并以电子出版物形式出版发行和提供信息服务。 ( 保密的学位论文在解密后适用本授权书) 学位论文作者签名：趁盘& 惫 指导教师签名： 日 期：巡哆日期： 学位论文作者毕业后去向： 工作单位： 通讯地址： 电话： 邮编： w 日 东北师范大学硕士学位论文 第一章引言 可满足性问题( s a t ) 已是倍受当代逻辑学界关注的重大问题，因为它们不仅具有 重要的理论价值，而且在人工智能、计算机科学、电子工程、工业生产等领域也有着广 泛的应用。许多其它领域的问题，如智能规划n 1 2 3 、微处理器证明口1 、工程技术、军事、 工商管理、交通运输以及自然科学研究中的6 0 0 0 余个重要问题，如程控电话的自动交 换、大型数据库的维护、大规模集成电路的自动布线、软件自动开发、机器人动作规划 等，都可以编码成s a t 问题，然后通过s a t 求解器。来求解。实验证明，这种间接求解 方法比问题原有的求解方法效率要高很多。s a t 问题是n p 完全问题，然而有许多趟领域 的问题是属于比n p 更难的复杂类，即卯复杂类，它们不能编码成s a t 问题。这类问题等 同于求解命题逻辑公式的可满足的模型个数，称这类问题为拌s a t 问题，如置信度分析问 题，一个表示成命题逻辑的没有确定概率信息的k b 和一个状态s ，以点留) 表示状态s 在 ，。 p r 、 k b 下的置信度，p ( 励) 三气新，m ( ) 表示模型( 可满足赋值) 的个数。贝叶斯 概率推理问题也可以转化成布尔公式的模型计数问题。 带量词的命题公式( q b f ) 可以看作是s a t 问题的推广，s a t 问题可以看作是所有 变量都是存在量词的特殊的q b f 问题。q b f 问题是p s p a c e 完全的，它比s a t 问题更难 求解。虽然如此，还是有许多学者致力于它的研究，目前已经提出了很多求解q b f 问题 的方法临刮并开发了许多有效的q b f 求解器n ，如q u a m e m 3 、y q u 棚e n 羽、q s a t n 射， s k i z z oc 1 4 3 等。由于q b f 问题具有丰富的表达能力，许多实际问题，如智能规划、信念修 正、非单调推理、知识推理等都可以转化成q b f 问题，然后用q b f 求解器来解决。然而 还有许多实际问题不能编码成q b f 问题，如寻找对手规划、象棋比赛、二人游戏赢的策 略个数问题，这类问题等同于求解命题逻辑公式的有效量化个数，称这类问题为拌q b f 问题，它们是拌p s p i a c e 完全的。 存s a t 问题是群p 完全问题的原型问题，拌q b f 问题是拌p s p a c e 完全问题的原型问题， 它们都是模型计数问题，两者虽属于不同的计算复杂类，但是r y a i l 、i l l i 踟s 证明了 群q b f 与拌s a t 复杂性相同，都是卯完备的。目前，已经开发了很多求解群s a t 问题的计数 器，但是并没有开发出求解拌q b f 问题的计数器。因为求解拌q b f 问题需要先求得公式的 所有赋值，然后推理得到所有的有效量化形式，这是一个比较复杂的过程，所以通常通 过求解 s a t 来间接的求解撑q b f 问题。 目前，大多数求解撑s a t 问题的模型求解器都是基于d p l l 方法n 明的，其中最早把 d p l l 方法用于模型计数的是b i n l b a u m 和l o z i l l s 虹i 【1 7 3 。后来，r o b e n o 等人在c d p ( d a v i s p u t l l 锄p r o o fp r o c e d u r e ) 方法1 7 。的基础上提出了d d p ( d e c o m p o s i n g d a v i s p l j 蜘a m ) 方法8 3 ，并对b a y a r d o & s c h r 喀提出的r e l s a t 算法9 3 进行了扩展，开发了r e l s a t2 模型求解器n 引，但是该方法效率不高。目前比较流行的是t s a n g 等人开发的c a c h 或啪3 求 东北师范大学硕士学位论文 解器和m a r cr n l u 订e y 开发的s i l a r p s a t m 。求解器。其中c a c h e t 啪。是利用组件缓冲和子旬学 习来计算模型的个数，后来此方法还加入了许多启发式，比如取样策略、组件选择策 略、变量分支选择策略、v s a d s 等来提高c a u c h e t 的性能。而s t l a r p s a l 则是利用高级组 件缓冲和蕴含布尔约束传播来求解模型的个数，这种技术的引入使得它在解决某些实例 问题时比c a c h e t 的效率还要高。目前，也有一些模型计数器是基于编译的，它们利用c 2 d 编译器倒把a 旺公式编译成o b d d 剀或是d - o b d d 晗5 。形式，然后再进行计算，这种方法 本质上和d p u 。算法相似。这些方法都是基于归结原理的。 本文提出了一类与归结原理相逆的# q b f 计数方法，基于扩展规则溉2 力的荐q b f 计数 方法。这类方法的基本思想是利用扩展规则把原公式扩展成和它等价的极大项组成的集 合，然后利用极大项的个数来进行撑q b f 计数，并利用容斥原理来解决空间复杂性问题。 这类方法与基于归结的方法相比，当包含互补文字的子句越多时效率越高，因此它可以 看作是和归结互补的方法。基于此思想，本文首先提出了一种基本的基于扩展规则的 存q b f 计数方法。然后，为了提高效率，本文还提出了一种改进的撑q b f 计数方法，即基 于知识编译嘲的方法，其思想是把要求解的问题应用扩展规则编译成e p c c l 语言，然后 再进行群q b f 计数。这种新方法与已有的知识编译方法的不同之处在于：无论是在线推 理过程还是离线推理过程都是基于扩展规则的。对于某些问题用此方法编译效率很高， 编译后的子旬集规模较小。最后，受组件分析n 町思想的启发，本文提出了基于组件分析 的存q b f 计数方法，其思想是把要求解的问题先分解成组件，然后对每个组件利用扩展 规则进行求解。由于该方法中还加入了单文字处理的功能，所以与前两种方法相比，它 不仅可以处理比较一般的拌q b f 计数问题，也可以处理规模较大的撑q b f 计数问题。 本文在给出算法的基础上，采用c + + 语言对算法进行了实现，设计了基于扩展规则 的三个拌q b f 计数系统：荐e r 、撑k c e r 和拌c s e r ，并用实例对其性能加以测试。结果表 明，挣c s e r 算法由于加入了单文字处理和组件分析的功能，使得它处理问题的能力比前 两种方法要好。由于目前国内尚没有一个公开成型的基于扩展规则的群q b f 计数器，所 以本文的三个系统特别是牟c s e r 系统将具有一定的研究价值与应用前景。这些方法在置 信度分析、贝叶斯概率推理删、对手规划、象棋比赛及二人游戏赢的策略个数问题等 方面有着重要的应用前景。 针对研究的内容，本文的结构安排如下： 第一章引言：首先概述了撑s a t 问题和群q b f 问题及二者的关系，然后列举了常用的 模型计数方法，最后介绍了本文的主要工作及本文的结构安排。 第二章智能规划概述：将概述智能规划的基本概念，发展及规划问题的间接求解 方法。 第三章可满足性理论扩展与应用：将首先简要介绍可满足性理论及其扩展，然后 介绍智能规划与拌q b f 的关系，最后对本文中常用的符号进行了说明。 第四章基于扩展规则的撑q b f 问题：将首先描述基于d p l l 方法的模型计数思想， 并介绍扩展规则的基本概念，然后介绍本文的主要工作：基于扩展规则的存q b f 计数方 2 东北师范大学硕士学位论文 法： 5 f e r 、存k c e r 和撑c s e r ，并对三种方法进行比较。 第五章三个拌o b f 计数系统的设计与实现：将首先简要介绍系统的设计及工作流 程，然后给出本文的实验过程，并对实验结果进行分析。 最后，将对本文所做的工作进行总结。 东北师范大学硕士学位论文 第二章智能规划概述 这一章主要包括智能规划的基本概念、发展及间接求解方法。虽然本文主要是研究 # q b f 计数问题，但笔者认为加上介绍规划的一章是必要的，因为群q b f 计数问题可看 作对规划求解问题的扩展，要想理解此项研究的意义，必先对规划有系统的了解，包括 其概念、发展及间接求解方法等。 2 1 智能规划的基本概念 智能规划是人工智能一个重要的领域，人们对它的研究已经有半个世纪之久。在人 工智能领域，规划目前还没有一个统一的定义。m c d e r n l 0 仕和j 锄e sh e n d e l e r 认为“规划 就是设计某个实体的动作序列，其结果被称为规划解 瞌新。d e e p a kk 啪a r 更加形象地 说“p 1 a r l i n g = h o wd 0ig e t 仃o mh e r et o 协e r e ? ”。直观地说，一个规划解实质上就是一个 动作序列，此序列能够实现某一目标，智能规划就是设计这个动作序列的过程，也就是 说它主要解决怎么做，而不解决为什么。它强调要有一个合理、周密的方案来有效地求 解问题。规划技术一般用于如何将原问题分解成适当的子问题，以及如何记录并处理在 问题求解过程中发现的子问题间的相互关系。 规划问题由于其自身的特点，它至少包括三个部分阻3 ：初始状态、目标状态和动作。 初始状态和目标状态是规划的起点和终点，动作是从初始状态到达目标状态的一系列可 执行的操作。初始状态和目标属于状态的描述，一般用一阶逻辑或命题逻辑来表示，动 作主要包括三部分：动作名称、动作前件和动作后件。如果一个动作的所有前件在一个 状态中得到满足，就称这个动作在这个状态中可用。 智能规划研究的主要目的是建立起高效实用的智能规划系统。该系统的主要功能可 以描述为：给定问题的状态描述、对状态描述进行变换的一组操作、初始状态和目标状 态。智能规划系统能够给出从初始状态变到目标状态的一个操作序列，其复杂性和所处 的环境与a g e n t 的功能有关。 2 2 智能规划的发展 智能规划研究开始于2 0 世纪6 0 年代，最早可以追溯到1 9 5 7 年n e w e l l 和s i m o n 的 问题求解系统g p s 。1 9 7 1 年f i k e 和n i l s s o n 的s t p s 系统在智能规划中具有划时代的 意义，该系统的知识表示方法和推理方法对后来的规划系统具有深刻的影响，但由于受 到当时客观条件的制约，该领域一直处于较为保守的状态，直到二十世纪8 0 年代后期， 随着客观条件的改善，此领域获得了长足的发展，在国防和空间技术领域中得到成功地 应用，取得了巨大的经济和社会效益。n a s a 于1 9 9 9 年在航天器“d e e ps p a c e0 n e ”中 运用规划技术，使得规划研究从实验室向实际应用迈出了重要的一步，标志规划的研究 4 东北师范大学硕士学位论文 步入了实用阶段，智能规划再次成为当前人工智能领域的研究热点。 对智能规划的研究已历经近半个世纪，其发展过程是曲折而复杂的，下面来概括一 下智能规划的发展路线：第一个主流规划器系统是s n u 口s ( f i k e s 和n i l s o n ，1 9 7 1 ) 汹 ， 它的整体控制结构以g p s 为模型，采用了q a 3 定理证明系统的一个版本作为用来确定行 动前提的真值的子程序，解决了框架公理问题，对推动规划技术的研究具有划时代的意 义。第二个规划器是n 忸a k ( c h 印m 趾，i 9 8 7 ) ，它是当时规划研究的一个逻辑重建和 简化工作：它的形式化表示足够清晰，允许证明规划问题的各种不同形式化方法的完备 性和不可操作性，但同时，它的出现也使人们认识到简单地利用定理证明的方法来解决 规划问题是很难的，因此，在1 9 9 0 年发现新的求解方法之前，对智能规划的研究陷入 了低谷。直到二十世纪8 0 年代后期，随着客观条件的改善，对于规划系统的研究达到 高潮。1 9 9 2 年，k a u t z 和s e l m a n 受到可满足性问题的贪婪局部搜索的意外成功的启发， 提出了可满足性规划和s a 邛i a n 算法u3 ，将规划问题翻译成命题可满足性问题加以解 决，实验证明，这种间接求解规划的方法比问题原有的求解方法效率要高很多。1 9 9 5 年，b l u m 和f u r s t 提出的缸a p h p l a n 方法口鳓，它描述了一个新的基于规划图的规划产生算 法，该算法比以往的算法都要快。它拥有许多重要的属性，如规划长度最优化、健壮、 稳定、合理、高效等优点。图规划的提出使得人工智能规划领域取得了革命性的进展， 该方法受到了研究者的广泛关注，并在其基础上做了大量研究，已取得了大量成果，如 i p p 、c g p 、t g p 以及p g p 等规划器都是在此基础上发展而来的。 2 3 规划问题的间接求解方法 这几年，智能规划的研究更是发展飞速，除了继续研究如何提高规划效率之外，学 者们还对如何扩展规划算法处理问题的范围，如何提高规划的质量进行了大量的研究。 1 9 9 2 年，k 脚s e l m a n 受到可满足性问题的贪婪局部搜索的意外成功的启发，提出了 可满足性规划和s a ：硎，a n 算法，将规划问题翻译成命题可满足性问题加以解决。实验 证明，这种间接求解方法比问题原有求解方法效率高很多。将规划问题转化为可满足问 题来求解的方法，是现代智能规划系统的5 大类方法之一，是与领域无关的智能规划算 法，代表规划系统有b l a c k b o x 口 。基于此理论的b l a c k b o x 规划系统在第一届智能规划 系统的比赛中表现了非凡的解决问题能力，开辟了解决规划问题的又一新途径。 将规划问题转化为可满足问题就是先把一个规划问题转化成一个已有有效算法或 过程的著名问题，然后对转化后的问题进行求解，最后从新问题的解中提取一个规划。 文献【3 8 】中简述了把规划问题编码为s a t 或c s p 问题的方法，这种编码方法的思想是先 把一个规划问题公式转化为一个命题可满足问题或其它的约束可满足问题，然后再利用 s a t 或c s p 算法求解，最后在解中提取规划解。 s a r 与c s p 算法的研究已经很深入，且有较成熟的有效的算法，目前不少算法已 经应用到解决规划问题中。这些算法的研究与不断改进，提高了规划解决相关重大问题 和复杂问题的能力。 东北师范大学硕士学位论文 第三章可满足性理论扩展与应用 3 1 可满足性理论概述 可满足性( s a r ) 问题是第一个被证明的n p 完全问题。它也是解决人工智能和计 算理论中许多实际问题的基础。可满足性问题：对于一个合取范式，是否存在该公式的 一组赋值，使其值为真。完成这种求解过程的软件或系统，被称为s a t 求解器。 带量词的命题公式( q b f ) 可看作是s a t 问题的推广，s a t 问题可看作所有变量都 是存在量词的特殊的q b f 问题。q b f 问题：给定一个合取范式，并对该公式中的变量 进行量化，判定q b f 是否为真。完成这种判定过程的软件或系统，被称为q b f 求解器。 3 2 可满足性理论的扩展 虽然对s a t 问题的研究已经取得了非常大的进步，然而有许多相关的逻辑问题仅判 定它的可满足性是不够的，它们是属于比n p 更难的复杂类，即卯复杂类。这类问题等 同于求解命题逻辑公式的可满足的模型个数，称这类问题为拌s a t 问题。拌s a t 是这样一 个函数，给定一个布尔公式f 作为它的输入，它会返回满足f 的赋值个数。它是 群p c o m p l e t e 的原型问题。 一 许多实际问题也不能编码成q b f 问题。如：寻找对手规划，象棋比赛，二人游戏 赢的策略个数问题，这类问题等同于求解命题逻辑公式的有效量化个数，称之为拌q b f 问题，它是；5 p s p l a c e 完全的。存q b f 是这样一个函数，给定一个布尔公式f 作为它的输 入，它会返回f 的有效量化个数。有效量化是指对一个公式的所有量词都进行量化，使 得到的量化命题公式的值为真。拌q b f 是拌p s p a c b c o m p l e t e 的原型问题。 3 3 智能规划与舟q b f 的关系 1 9 9 2 年，k a u t z 和s e l m a n 受到可满足性问题的贪婪局部搜索的意外成功的启发，提 出了可满足性规划和s a t p n 算法 ，将规划问题翻译成命题可满足性问题加以解决。 实验证明，这种间接求解的方法比问题原有的求解方法效率要高很多。 然而到目前为止，所有的规划求解器无论是直接还是间接的求解规划问题，最终只 能求解问题的一个解，不能求解问题的所有解个数，如对手规划，二人游戏赢的所有策 略数等实际问题。虽然这些问题可以通过相应的处理器( b l a c k b o x 碍7 3 ) 转化成群q b f 问 题，但目前还没有开发出 q b f 求解器。因为求解拌q b f 问题需要先求得公式的所有赋值， 然后推理得到所有的有效量化形式，这是一个比较复杂的过程，所以通常通过求解拌s a t 来间接的求解撑q b f 问题。由于r y a n w i l l i a n l s n 5 3 已经证明了拌q b f 与群s a t 复杂性相同，都 是卯完备的，这样就可以用已经开发的拌s a t 求解器来求解撑q b f 问题，当然我们也可以 6 东北师范大学硕士学位论文 开发自己的撑q b f 求解器。 3 4 本文中的一些约定 对本文中符号的一些约定：用，：，表示c n f ( c o 玛u i l c t i v en o 衄a 1f o m ) 形式的子句集。用c ，c ，c ：，表示单个的子句，有时也把子句理解成文字集合 的形式。通常m 表示一个子旬集中所有原子的集合。为了方便理解，首先给出与本 文相关的概念。 可满足性：如果一个子句的变量在某些赋值下为真，则称该子旬是可满足的。如果 一个公式f 中所有的子句在一组赋值下都可满足，则称该公式f 是可满足的。这样的一 组赋值称为公式f 的一个解。 s a t 问题就是给定一个包含n 个布尔变量( 只能为真或假) x ，x ：，x 。的逻 辑合取范式，是否存在它们的一个取值组合，使得该合取范式被满足。 q b f 是s a t 闯题的推广。它的形式如下： q l xj q 。x 。f ( x 1 ，x 。) ( 1 ) 其中，f 是一个包含命题变量x ，x 。的命题公式，q ，或者是存在量词j ，或者是全 称量词v 。因为v x f 伍y ) = v y v x f y ) ，j x j y f y ) = j y j ) 【f 随y ) ，所以可以把变量 分成不同的集合，每个集合由具有相同量词属性的相邻变量组成。因此公式( 1 ) 也可 以写成下面的形式： q 1 x 1 q 。x 。f ( x l ，一，x 。) ( 2 ) 其中，x 是变量的集合，每个x 之闯没有交集。公式中的每个变量必须属子某一个变 量集合，我们根据变量所属集合的量词属性来判定变量的属性。如 v 州b v c j 妇y f b ，c ，x ，y ) 可以简写成v a b c j x y f b ，c ，ky ) 。如果公式f 是一个合取范式 ( q 妤) ，q b f 的形式就变成了 q l x l q 。x 。c 1 ，c 2 ，c m ( 3 ) 其中c i 是一些子句。我们称这种形式的q b f 为c 型q b f 。在无特别说明的情况下， 本文都是指这种形式的q b f 。 q b f 求值问题就是给定一个q b f ，判定它是否满足。如：v 妇y ( x + y ) n x + 1 y ) 表 示当给x 赋任意真值时是否存在真值赋于y 使得( x + y ) h x + 一y ) 满足，如臬存在真值赋 于y 使得公式满足，则这个q b f 的值为真，否则它的值为假。这类问题与给定一组赋 值和一个f ，判定f 在这组赋值下是否为真的s a t 判定问题相似。q b f 问题是 p s p a c e - c o m p l e t e 的，这是一类比n p c o m p l e t e 问题更难求解的问题。 荐s a t 是这样一个函数，给定一个布尔公式f 作为它的输入，它会返回满足f 的赋 值个数。 ， 撑q b f 是这样一个函数，给定一个布尔公式f 作为它的输入，它会返回f 的有效量 化个数。有效量化是指对一个公式的所有量词都进行量化，使得到的量化命题公式的值 7 东北师范大学硕士学位论文 为真。 拌s a t 是撑p c o m p l e t e 的原型问题，即所有的存p 问题都可以通过卯归约化成拌s a t 问题。撑q b f 是杼s p a c e c o m p l e t e 的原型问题，即所有的拌p s p a c e 问题都可以通过群p 归约化成群q b f 问题。两者复杂性相同，都是抑完备的。 东北师范大学硕士学位论文 第四章基于扩展规则的拌q b f 问题 从这一章开始，我们将系统地介绍本文的主要工作基于扩展规则的拌q b f 计数 方法及其实现。 在这一章中，将分三个部分对本文中的方法加以介绍。首先介绍目前常用的模型计 数方法，第二节介绍扩展规则的相关概念，第三节分别介绍三种基于扩展规则的拌q b f 计数方法，并对三种方法进行比较。 4 1 基于d p l l 方法的模型计数 目前，大多数的模型求解器都是基于d p l l n 6 3 方法的，也有一些模型计数器是基于 编译的，它们利用c 2 d 编译器3 把c n i ? 公式编译成o b d d 幢4 3 或是d o b d d 口5 3 形式，然后再 进行计算，这种方法本质上和d p l l 算法相似。 d p l l 算法求解模型个数的基本思想不是直接寻找原公式的一个模型，而是在f 中 任选一个变量x ；，公式( f x i ) 和公式( f 八 x ；) 的可满足赋值也是公式f 的可满足赋 值，并且这两个子公式所得的解没有交集。这样原公式的解可以表示成如下的形式：。 m ( f ) = m ( f x i ) + m ( f 1 x j ) 其中m ( f ) 表示公式f 的模型个数。 。 这两个子公式可以通过单元传播进行化简，但是在公式f 中出现的变量可能不出现 在化简之后的子公式( f 八x i ) 和公式( f 入1 x i ) 中，如果在f 中有n 个变量，( f x i ) 中 有n + 个变量和公式( f 八1 x i ) 中有n 。个变量，那么， m ( f ) = m ( u n i t p r o p ( f x i ) ) 2 n 。矿+ m ( u n i 印r o p ( f 1 x j ) ) 2 ”。 其中，n n + 个自由变量和n n 个自由变量可以取o 也可以取1 。 b a v a r d o 和p e h o u s h e k n 町中提出了通过组件分析来求解模型个数的方法。他们用一个 连接图来表示一个公式f ，图中的结点都是公式f 中的交量，如果两个变量出现在同一子 旬中，则这两个变量之间有边相连。如果公式f 通过连接图可以分解成子公式f ：，e ， e ，那么 上 m ( f ) = i im ( f i ) 百 。 因此，在选择一个变量对它进行赋值之前应该先把要处理的公式分解成组件，每个 组件的模型采用d p l l 计数器进行求解。 不管是基于d p l l 算法的计数方法，还是基于编译的计数方法，它们本质都是基于 归结原理的。本文与之不同，提出了应用扩展规则来求解稃q b f 问题的方法，这是一种 与归结原理相逆的方法，这种方法有时从效率上要优于基于归结的方法，因此可以看作 是和归结互补的一种方法。 东北师范大学硕士学位论文 4 2 扩展规则的基本概念 本文中采用了与常用的基于归结的推理规则相逆的方法，即基于扩展规则的方法来 求解群q b f 问题。林海在文献【2 6 】中对扩展规则进行了详细的阐述，下面对本文涉及到 的与扩展规则有关的内容进行说明。 定义4 1 汹3 给定一个子句a 和一个原子的集合m ： b = a v c ，a v l cl c m 并且c 和1 c 都不出现在a 中) 从a 到b 子句集的推导过程叫做扩展规则，b 中的子句叫做应用扩展规则的结果。 例如，给定一个子旬c 和集合( c ，d ) ，应用扩展规则韵结果就是c v d 和 c v 1 d 。下面来看一下子句a 和它扩展之后的结果b 之间的关系。 定理4 1 蜥子句a 和它扩展后的结果子句集b 是等价的。 证明：因为由b 经过一步归结可以得到a ；而a 可以推出b 中的任意一个子句，即a 能推出b ，所以a 和b 是等价的。 这样，我们可以对子旬集中的子句应用扩展规则。定理4 1 保证了应用扩展规则后 的子句集和原子句集等价。因此扩展规则可以被看作是一条推理规则。 ， 定义4 2 3 一个子句包含了集合m 中的所有原子，并且每个原子在该子句中或是以正的 形式出现或是以负的形式出现，则称该子句是集合m 的极大项。 如果子句集中所有的子句都是极大项，一个子句只有和它的否定放在一起才是不可 满足的。例如：如果子句集中缺了子句a i ，一a 。只有和a i 放在一起才不可满足，而 子句集当中恰好没帝a ；，因此子句集可满足，1 a i 可以看作子句集的一个模 型，即子旬集中缺少的极大项的个数就是子句集的有效量化个数。由此可以推理 得到如下求解有效量化个数的定理。 定理4 2 给定一个子句集，它其中所有原子的集合是m ( i m = 姐) ，如果子旬集中 的子旬都是m 上的极大项，并且子句集包含s 个不同的极大项子句，那么满足这个 子句集的有效量化个数就是子句集中所缺少的极大项子旬的个数，为2 “s 。 如果给定的子句集中包含的子旬不全是m 上的极大项，那么我们需要根据扩展 规则把所有非极大项的子句扩展成极大项，然后应用定理4 2 来求解子旬集的有效量 化个数。 然而我们发现，直接应用扩展规则最坏情况下的空间复杂性是指数级的。实际上我 们并不需要把所有的极大项都扩展出来，只需要计算它们的个数就足够了。为了避免空 间爆炸，我们引入了容斥原理。 定理4 3 ( 容斥原理) 集合a ，a ：，a 。并集的元素个数可以用如下公式计算： 1 0 奎! 垦塑垄奎兰堡主兰垡笙奎 l a lu a 2u u a n l - i a i 卜l a in a j i + + ( 1 ) n + 1 i a lr 、a 2n n a n i i - l k i 舞n 容斥原理的简单形式为： | au b | - | a + f b 一| an b ， i a u b u c i = l a i + i b l + c j - | a r 、b 卜l a n c i - f b n c l + i a n b 厂、c | 。在介绍如何应用容斥原 理求解一个子句集扩展出的极大项的个数之前还需要介绍下面的定理。 定理4 4 当且仅当两个子旬含有互补对时，两个子句扩展出的极大项的集合不含交集。 证明：充分性：假设两个子句含有互补对( 假设为a 和1 a ) ，则在含有a 的子旬扩展 出来的极大项中，a 一定是以正的形式出现，在含_ 1 a 的子句扩展出来的极大项中，a 一定是以负的形式出现。因此，两者一定不有含交集。 必要性：( 反证法) 假如两个子句不含互补对，则这两个子句的并集对应的子句能被两 个子句都扩展出来，因此，它们含交集。而如果两个子句扩展出的极大项的集合中不含 有交集，则它们一定含有互补对。 给定一个子句集= a l ，a ：，a 。) ，m 是其原子的集合且 m i = m 。记p 为a i 扩展出的所有极大项的集合，i = l ，n 。令s 为能扩展出的所有极大项的集合的 子句个数。则s = l p lup 2u up n l ，由容斥原理可以得到跚： s = i 尸，l 一i 毋n 弓i +l 鼻厂、弓n 毋l 一+ ( 一1 ) 时1l 毋n 逻广、n 最i ( 公式1 ) ，= 1 l 彰 歹s 力l s l 歹 ，匀2 其中，吲= 2 扩 。r o a t 和a j 中含有互补对。 ip inp j l = 。f l2 扰一1 4 u 4 i ， a ；和a 。中不含互补对。 上式中，| p f 的计算比较好理解：a j 中含有l a 个原子，在扩展出的极大项中，剩 余的m l a 。1 个原子可以任意为正或为负，所以j p i 是2 俨川个；l p ir 、p j f 的计算是这样 的：两个子句扩展出的极大项不含交集当且仅当它们含有互补对。因此，当两个子句a ，、 a j 含互补对时，lp inp j i 为o 。否则，i p jnp j f 为2 班_ 1 4 u 4 j 。 4 3 基于扩展规则的群q b f 计数方法 本文提出了一类新的求解拌q b f 问题的方法，即基于扩展规则的拌q b f 计数方法。 这类方法的基本思想是利用扩展规则把原公式扩展成和它等价的极大项组成的集合，然 后利用极大项的个数来进行毋q b f 计数，并利用容斥原理来解决空间复杂性问题。基于 此思想，本文提出了三种具体的基于扩展规则的拌q b f 计数方法，下面分别对这三种方 法进行详细介绍。 l l 东北师范大学硕士学位论文 4 3 1 基本的基于扩展规则的样啷计数方法：祝r 方法 根据上述基于扩展规则迸行群q b f 计数的基本思想，本文设计了基