A QBF Solver Based On Survey Propagation

Recently, more and more researchers focus on intelligent planning. The planning solution based on propositional logic formula is one of the most important methods of researching intelligent planning.One of the propositional logic formulae is Quantified Boolean Formulae, which can be seen as an extension of Satisiability (SAT) with existential or universal quantifiers to every variable in propositional formulae. Given a Quantified Boolean Formula, the question of deciding the satisfiability of the formula is called a Quantified Boolean Satisfiability problem (QBF). QBF is an important issue in AI because it is the prototypical problem complete for a complexity class, i.e. PSPACE. Thus, many practical problems can be transformed into QBF, e.g. conformant planning, verification, non monotonic reasoning and reasoning about knowledge.In this thesis, we present a novel DPLL-based solver for Quantified Boolean Formulae (QBF), namely SPQBF. To the extent of our knowledge, this solver is the first QBF reasoning engine that incorporates Survey Propagation method for problem solving. Using the information obtained from the survey propagation procedure, SPQBF can select a branch more exactly. Furthermore, when handling the branches, SPQBF uses some efficient technologies for solving QBF problems more efficiently, such as unit propagation, conflict driven learning as well as satisfiability directed implication and learning. The experimental results also show that SPQBF can solve both random problems and QBF benchmark problems efficiently, which validates the effect of using Survey Propagation in QBF solving process.