Research Of The QBF Solver Based On Knowledge Compilation

Intelligent planning is an important branch in artificial intelligence, has been widely used in many fields. An important way for solving intelligent planning problem is translating it into propositional logic to solve. The planning of determinate action and state can be translate into classic propositional logic (SAT) to solve; the planning with determinate action and indeterminate initial state can be translate into Quantified Boolean Formulae (QBF) to solve. QBF is a generalization of SAT, it can solve consistency planning with large state space. As a standard PSPACE-complete problem the importance of QBF in artificial intelligence is growing. Many problems in artificial intelligence as non-monotonic reasoning, parallel consistent inference can be converted into QBF in polynomial time, and experimental data shows that the transformation-based approach is more effective than domain dependence method.Knowledge Compilation emerged in recent years as a new research direction; it is used to deal with the computational complexity of propositional logic. According to this method, reasoning process is divided into two stages: Off-line compilation phase and on-line inquiry stage. Off-line, propositional logic has been compiled into some tractable target language; on-line, target language is used to effectively answer the exponential number of queries. The main motivation of knowledge compilation is putting the main expense on the off-line stage, using for numerous Effective off-line query to offset, and generate a fast online inference system. Knowledge compilation has been used in SAT, and achieved good results, QBF is a generalization of SAT, and knowledge compilation can also be used in QBF.In this paper we discuss the basic property, completeness, the operation of query and translation and succinctness of EPCCL, FNNF, OFNNF, D-FNNF, D-OFNNF. On the basis of OFNNF's property, we raise a new approach for model counting, we call it tableau model counting. According to the discuss of the five target language, we choose two of them OFNNF and D-OFNNF, design compiler for them, add compatibility on them, then use them as the martrix of QBF, this makes the QBF can be solved in polynomial time, and give the corresponding algorithm, we design a solver for QBF with knowledge compilation.