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