量化布尔公式的理论与算法研究

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