QBF求解算法研究综述

近10年来，布尔可满足性(SAT)求解技术飞速发展，并已经成功应用于模型检验、定理证明等领域，特别是在限界模型检验(BMC)中取得了明显的进展，然而，由于命题逻辑公式的长度随系统规模指数倍增长，基于SAT的模型检验仍然存在状态空间爆炸问题.带量词的布尔公式(QBF)作为SAT公式的自然扩展，具有紧凑的空间结构、更强大、更直观的表达能力，能够简洁地描述模型检验中的公式.基于QBF的模型检验有希望缓解状态空间爆炸问题，成为当前研究的一个热点.总结了当前主流的QBF求解算法及常用的优化技术，指出了该领域中值得关注的新趋势.

Survey on QBF Evaluation Algorithms

Dramatic improvements in Boolean satisfiability (SAT) solver technology over the past decade have led to mass applications of SAT in formal verification. SAT methods have been applied in model checking and theorem proving in a variety of ways. More recently, bounded model checking (BMC) has highlighted the potential for symbolic techniques based on SAT. However, usage of propositional formulas imposes a potential exponential memory blow-up on the SAT-based model checking algorithms due to the big formula sizes. As a natural extension of SAT, quantified boolean formulas (QBF) which captures a wider class of problems in a natural and compact way allows an exponentially more succinct representation of the checked formulas. Model checking based on QBF solvers have recently emerged as a promising solution to reduce the state explosion problem. However, practical experiences show that compared with SAT-based approaches, QBF-based method has invariably yielded unfavorable experimental results, because of the lack of an efficient decision procedure for QBF. Many QBF solvers are obtained by extending satisfibility results; however, experiences show that although search-based algorithms are considered to be the most efficient approaches to SAT, decision paradigms other than search may have more chances to succeed in QBF than they had in SAT. This paper presents a survey of the latest developments in algorithms and optimizations of QBF evaluation, and summarizes some noteworthy trends in this area.