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.