The Research On QBF Solver Based On Backdoor Sets Via Local Search

Recently, intelligent planning is focused on the more and more researchers in artificial intelligence focus on. Up to the present, one of the important approach of solving intelligent planning is compiled planning problem to SAT problem, and then utilizing high efficient SAT solver to resolve it.The propositional satisfiability problem (SAT) is an important issue in AI. Given a propositional logic formula, the propositional satisfiability problem (SAT) is a process of deciding the satisfiability to formula. SAT problem is more difficult to solve, i.e. which computational complexity is NP-complete. The hidden structure of instances-a backdoor set of variable can improve the efficiency of SAT problem.One example of such hidden structure is a backdoor set of variable for SAT, which captures the link between dependencies among backdoor variables and problem complexity. A backdoor set of formula F is a subset B such that if the assigns to the variables in B certain truth values, then the simplified instance belong to a class C of instances that can be solved in polynomial time. Because of its importance in solving complex problems, the research of backdoors has become research focus in recent years. The method of solving backdoors has been extended to the QBF problem currently.Quantified Boolean Formulae can be seen as the generalization of Satisiability (SAT) with existential or universal quantifiers to every variable of propositional formulae. QBF problem is more difficult to solve than SAT problem, i.e. which computational complexity is PSPACE, and which plays an important role in AI. The introduction of backdoors can improve the efficiency of QBF problem.In this paper, we give a general overview of the existing algorithms of a backdoor set for problem instances, then present a new algorithm of computing backdoor set for QBF bases on renamed variable and use the backdoor set to QBF solver for the first time to design a new QBF solver– BDQBF system. According to the process of computing the backdoor set, BDQBF can select a branch more exactly, and this can reduce the search space and the number of back-off of QBF problem, and then improve the efficiency of solving QBF problems. Furthermore, we illustrate the advantages of our algorithm through several real-world QBF instances. The experiments are carried out on VC++ operation platform and RedHat ES3.0. Experimental result show that this algorithm can compute the smaller backdoor sets for QBF problems and the backdoor sets computed can improve the efficiency of solving QBF problems.