智能规划已经成为人工智能的研究热点,把智能规划问题转化为命题逻辑公式求解是研究智能规划的重要方法。量化布尔公式(Quantified Boolean Formulae,简称QBF)是一种带有存在和全称量词前缀的命题逻辑公式。当QBF公式的量词中只含存在量词时,QBF问题就转化为命题可满足(SAT)问题。因此QBF问题通常可以看作是SAT问题的泛化。判断一个量化布尔公式的可满足性需要判断是否存在一组命题变量的真值指派,使得公式在该真值指派下为真。判断量化布尔公式问题的可满足性的计算复杂性要高于SAT问题,是PSPACE完备的。随着QBF问题的求解效率不断提高,QBF问题在诸如一致性规划、验证、非单调推理、知识推理等方面都有着广泛的应用。本文设计了一种新的基于DPLL算法的QBF求解器—SPQBF系统。它将Survey Propagation信息传递方法第一次应用到QBF求解问题中。把Survey Propagation作为启发式,引导DPLL算法选择合适的变量进行分支,从而可以减小搜索空间,并减少算法回退的次数。在分支处理过程中,SPQBF系统结合了单元传播、冲突学习和满足蕴涵学习等一些优秀的QBF求解技术,从而可以提高QBF问题的求解效率。实验结果表明,SPQBF无论在随机问题上还是在QBF标准测试问题上都有很好的表现,验证了调查传播技术在QBF问题求解中的实际价值。