Research On The Knowledge Compilation Method Based On The EPCCL Theory

Knowledge representation and reasoning is an important research area of artificial intelligence, which is based on the idea that an agent stores what it knows in a knowledge base, typically using a logical formalism, and then in the practical applications specific algorithms for querying are called to extract information implicitly stored in the knowledge base. It is well known reasoning problems in their general form are intractable. In fact, problems in logic are known among computer scientists for their high computational complexity. For example, if the knowledge base and the query are represented in first-order logic, then checking whether the query is logically entailed by the knowledge base or not is the prototypical recursively enumerable, non-recursive problem. Checking the logical entailment between two propositional formulae faces a co-NP-complete problem.Knowledge compilation has been emerging recently as a new direction of research for dealing with the intractability of reasoning problems. The idea of this approach is to split the reasoning process into two phases: an off-line compilation phase, in which the propositional theory is compiled into some tractable target language, and an on-line query-answering phase, in which the compiled target is used to efficiently answer the queries. And the compiling time in off-line phase can be amortized by a (potentially) exponential number of on-line queries.The target language is one of key aspects for any compilation approach. There have existed many target languages so far, such as Horn theories, prime implicates/implicants, ordered binary decision diagram, decomposable negation normal form (DNNF), EPCCL theory and so on. The EPCCL theory was proposed by Lin Hai and Sun Jigui in 2004. And an extension rule based EPCCL compilation algorithm called KCER was also devised. Based existing work, we further study the compilation method based on the EPCCL theory and the main contributions are listed as follows:(1) Propose a new EPCCL theory compilation framework, based on three different factors, including the way to divide a CNF formulas into two parts, the way to compile the disjunction of a CNF formula and a DNF formula, and the way to transform a DNF formulas into an EPCCL theory, this framework can be evolved into a lot of different compilation algorithms. On this basis, we propose two algorithms DNF2EPCCL-DPLL and DNF2EPCCL-OR which can transform a DNF formulas into EPCCL theory, and based on this framework we devise three distinctive compilation algorithms KCDP, KCMS and KCOR. (2) In order to compare the EPCCL theory with other target languages and apply the EPCCL theory in practical applications, the EPCCL theory is added to the compilation map according to three key dimensions: the succinctness of the EPCCL theory, the class of queries that the EPCCL theory supports in polytime, and the class of transformations that the EPCCL theory supports in polytime. And we obtain the following conclusions: EPCCL≤CNF does not hold unless the polynomial hierarchy collapses; EPCCL≤IP, EPCCL≤DNF, EPCCL≤NNF, EPCCL≤OBDD<, EPCCL≤OBDD, EPCCL≤FBDD, EPCCL≤d-DNNFT, EPCCL≤d-DNNF, EPCCL≤DNNFT, EPCCL≤DNNF and MODS≤EPCCL do not hold, EPCCL≤MODS and CNF≤EPCCL hold; the EPCCL theory satisfies CO, VA, CE, IM, BC and SFO; the EPCCL theory don't satisfy FO; the EPCCL theory don't satisfy∧C unless P = NP; if the EPCCL theory satisfies ?C,then it satisfies∧BC.(3) As the size of the EPCCL theory is directly related to the efficiency of the online query-answering, the reduction rule is proposed to reduce the size of EPCCL theory. And based on this rule, an algorithm called REDUCE with polynomial time complexity is devised. Finally, we devise an EPCCL compiler C2E to combines the strength of KCDP and REDUCE, and we test its performances on the random instances and benchmarks. The experimental results show that C2E is an excellent EPCCL compiler. It should be pointed out that the current efficient DPLL based SAT solvers have made use of a lot of advanced technologies, which can be introduced into the C2E. In the same time, we are also able to design some heuristic functions to speed up KCDP. So C2E still has the huge potential enhancements.(4) Propose the extension rule based model counting algorithm #ER and prove that #ER can count the models of an EPCCL theory in linear time. Furthermore, develop the algorithm #CDE, which is a combination of #ER and #DPLL. Experimental results show that #ER outperforms #DPLL on a wide range of problems and #CDE integrates advantages of #ER and #DPLL. Taking into account that there exist a set of analogous CNF formula being counted in practical applications, in contrast with solving these SAT problems separately, we develop an algorithm called #ERS that solves them as a whole. In the #ERS algorithm, the same part and the different part in the set of CNF formula are compiled into the EPCCL theory respectively. Finally, the above algorithms are tested by random CNF formulae. Experimental results show that #ER outperforms #DPLL on a wide range of problems, #CDE integrates advantages of #ER and #DPLL and #ERS behaves efficient for the CNF formulae set with high close factor.