基于扩展规则的＃QBF求解系统的研究及实现

摘要

智能规划是设计某个(组)实体从初始状态出发，到达目标状态的动作序列，其结果被称为规划解。目前的规划求解器只能求解问题的一个解，不能求解问题的所有解的个数，如对手规划，二人游戏赢的所有策略数等问题。虽然这些智能规划问题可以通过相应的处理器(BlaekBox)转化成＃QBF问题进行求解，但是目前还没有开发出＃QBF求解器。 针对这一问题，本文提出了一类新的求解＃QBF问题的方法--基于扩展规则的＃QBF计数方法，用来求解相应的智能规划问题。这类方法的基本思想是利用扩展规则把原公式扩展成和它等价的极大项组成的集合，然后利用极大项的个数来进行撑QBF计数，并利用容斥原理来解决空间复杂性问题。这类方法与基于归结的方法相比，当包含互补文字的子句越多时效率越高，因此它们可以看作是和归结互补的方法。基于此思想，本文首先提出了一种基本的基于扩展规则的＃QBF计数方法；然后，为了提高效率，本文还提出了一种改进的＃QBF计数方法，即基于知识编译的方法，其思想是把要求解的问题应用扩展规则编译成EPCCL语言，然后进行＃QBF计数；最后，受组件分析思想的启发，本文提出了基于组件分析的拌QBF计数方法，这种方法的思想是把要求解的问题先分解成组件，然后对每个组件利用扩展规则进行求解。由于该方法中还加入了单文字处理的功能，所以与前两种方法相比，它不仅可以处理比较一般的＃QBF计数问题，还可以处理规模较大的＃QBF计数问题。 在给出算法的基础上，本文采用C++语言对算法进行了实现，设计了基于扩展规则的三个＃OBF计数系统：＃ER、＃KCER和＃CSER，并用实例对其性能加以测试。实验结果表明，在处理一般问题时，＃ER的时间复杂性是指数级的，效率比较低；＃KCER算法理论上要优于＃ER算法，但是经过编译后的子句集扩大的规模在最坏情况下是指数级的，所以它的效果也不尽如人意；＃CSER算法由于加入了单文字处理和组件分析的功能，使得它处理问题的能力比前两种方法要好。由于目前国内尚没有一个公开成型的基于扩展规则的＃QBF计数器，所以本文的三个系统特别是＃CSER系统将具有一定的研究价值与应用前景。

目录

文摘

英文文摘

声明

第一章引言

第二章智能规划概述

2.1智能规划的基本概念

2.2智能规划的发展

2.3规划问题的间接求解方法

第三章可满足性理论扩展与应用

3.1可满足性理论概述

3.2可满足性理论的扩展

3.3智能规划与#QBF的关系

3.4本文中的一些约定

第四章基于扩展规则的#QBF问题

4.1基于DPLL方法的模型计数

4.2扩展规则的基本概念

4.3基于扩展规则的#QBF计数方法

4.3.1基本的基于扩展规则的#QBF计数方法：#ER方法

4.3.2基于知识编译的#QBF计数方法：#KCER方法

4.3.3基于组件分析的#QBF计数方法：#CSER方法

4.3.4三种方法的比较

第五章三个#QBF计数系统的设计与实现

5.1系统介绍

5.2系统功能设计

5.3系统基本类的设计

5.3.1子句

5.3.2子句集

5.3.3组件集

5.4各结构类之间的关系

5.5系统工作流程

5.5.1#ER方法的工作流程

5.5.2#KCER方法的工作流程

5.5.3#CSER方法的工作流程

5.6开发工具及测试环境

5.7实验结果及分析

结 论

参考文献

致谢

在学期间公开发表论文情况