论文部分内容阅读
智能规划是人工智能中比较热门的研究领域之一,目前智能规划求解的主要方法之一是将智能规划问题转化为命题可满足问题(Propositional Satisfiability Problem,简称SAT),然后利用高效的SAT求解器进行求解。命题可满足性问题(简称SAT)是当今人工智能研究的核心问题。SAT问题可以描述为给定一个命题逻辑公式,其变元是否存在一个真值赋值使命题公式成立(可满足),如果成立则返回这些变元的真值赋值。SAT问题是比较难求解的问题,其计算复杂性是NP完备的,而实例的隐藏结构能够找到有效的SAT求解方法,Backdoors就是这种隐藏结构之一。隐蔽集(backdoor sets)是SAT问题的一个重要的隐藏结构,与问题难度有很大的关系。它的选择能使剩下的问题在多项式时间内求解。隐蔽集可以描述为一个较小的变量子集B,对B中的变量进行真值指派后,简化后的公式可以在多项式时间内求解。由于其在复杂问题求解中的重要性,近年来隐蔽集的研究已逐步成为研究的热点。目前隐蔽集的求解方法已经扩展到QBF问题中。量化布尔公式(Quantified Boolean Formulae,简称QBF)是一种带有存在量词和全称量词前缀的命题逻辑公式。当QBF公式中的量词中只含存在量词时,QBF问题就转化为SAT问题。因此QBF问题可以看作是SAT问题的泛化。QBF问题是比SAT问题更加难解的问题,其计算复杂性是PSPACE完备的。隐蔽集的引入能提高QBF问题的求解效率。本文首先对现有的隐蔽集问题的求解算法进行一个总体的概述,其次针对QBF问题设计了一种新的基于重命名的隐蔽集求解算法,并将隐蔽集首次应用到的QBF求解器中从而设计出一种新的BDQBF求解器。在BDQBF中,我们用隐蔽集中的变量作启发式,引导算法进行分支搜索,从而减小了算法的搜索空间和回退次数,并提高了QBF问题的求解效率。最后本文针对这一算法进行了两类实验:第一类实验是在Windows环境下用标准的C++实现这一算法,并与原有求解QBF问题的隐蔽集算法进行了比较,结果表明这一算法能求解出问题的较小隐蔽集;第二类实验是在Linux环境下用标准C++语言实现了QBF问题求解器BDQBF系统。结果表明无论是QBF的随机问题还是标准测试问题,BDQBF求解器都有很好的求解效果。这些实验验证了隐蔽集在QBF问题求解中的实际价值。