Approximate Knowledge Compilation For Quantified Boolean Formulas

Nowadays, intelligent planning is becoming more and more important in the research domain of artificial intelligence,moreover, the most vital method for solving intelligent planning is that we firstly convert the planning problems into Quantified Boolean Formulae, then we solve the QBF problems efficiently. In fact, automate reasoning is also an important research direction in artificial intelligence, and knowledge compilation is one of the most efficient approach for dealing with reasoning problems. However, most methods for knowledge compilation are based on propositional logic.Quantified Boolean Formulae is an important issue in AI. QBF Formulae is propositional logic formulae with existential or universal quantifiers to every variable in prefix. Though it is the prototypical problem complete for a complexity class, i.e. PSPACE, the expression of QBF is much better than propositional logic formulae, as a result, many subclass of QBF can be used as target languages for knowledge compilation.This paper aims to further improve the knowledge compilation of propositional logic, so that it can deal with the QBF knowledge bases. We present an approximate knowledge compilation, which select the QHorn theory-the subclass of QBF-as the target language. Above all, the concept of QHorn approximates are defined, secondly we propose two algorithms, algorithm QHorn-GLB, which computes the QHorn greatest upper bound of original QBF knowledge base, and algorithm QHorn-UB, which computes the QHorn upper bound of original QBF knowledge base, thirdly the proof of correctness for these two algorithms are provided, finally we use these approximations to improve the efficiency of knowledge compilation. Experimental results show that this method can effectively deal with the knowledge compilation for QBF problem, and can answer the query about original knowledge base in polynomial time.