量化布尔公式(QBF)的研究近二十年来显得越来越重要了。一方面在计算复杂性理论中它刻画了一个自然的复杂度类(PSPACE)。另一方面,计算机科学和人工智能领域中的诸多问题,例如规划问题,硬件检测,程序验证,知识推理等等,都可以转换成QBF公式的可满足性问题。例如,C.Castellini等人开发的QBF Solver已成功用于行为的规划问题;A. Abdelwaheb也研究出了基于QBF的硬件检测工具。然而,和通常的可满足性(SAT)问题相比,QBF的可满足性(QSAT)问题的研究严重滞后,QBF 工具的应用也面临着很大的挑战。目前仍有142类随机产生的或来源于实际问题的QBF公式,利用现有的QBF solver 还无法解决它们的可满足性。因此,对QBF问题的理论和算法研究引起了人们的极大关注。本项目将通过研究QBF的模型理论、结构特性等,发现并设计更高效实用的解决QBF问题的算法。