基于调查传播方法的QBF求解器

摘要

智能规划已经成为人工智能的研究热点，把智能规划问题转化为命题逻辑公式求解是研究智能规划的重要方法。 量化布尔公式(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问题求解中的实际价值。

目录

文摘

英文文摘

声明

引 言

第一章智能规划

1.1智能规划概念

1.2智能规划的应用

1.2.1航空航天领域中的应用

1.2.2机器人领域中的应用

1.2.3智能工厂中的应用

1.2.4商业中的应用

1.3智能规划的发展

1.4规划问题编码为逻辑命题公式

1.5论文结构

1.6论文主要工作

第二章QBF问题

2.1相关概念

2.2 QBF问题与SAT问题比较

第三章SPQBF算法框架

第四章基于Survey Propagation方法的分支选择

4.1自旋玻璃和SAT

4.2 SP方法的基本原理

4.3利用Survey Propagation进行分支选择

4.3.1因子图(Factor Graph)

4.3.2消息传递

4.3.3基于Survey Propagation的分支选择

第五章分支处理

5.1冲突推理

5.2冲突学习

5.3满足蕴涵学习

第六章实验比较

6.1 DPLL算法和SPQBF算法比较

6 2 SPQBF和参赛QBF求解器效率比较

第七章总结

参考文献

后 记

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