Research On The Efficient Methods Of Knowledge Compilation Based On The Hyper Extension Rule

Extension rule-based reasoning method is proposed as a novel reasoning method in2003, it has been widely recognized by domestic and foreign scholars. Newalgorithms of reasoning and knowledge compilation can be designed based on ER. Weintend to improve the efficiency and quality of knowledge compilation based on ER.The quality of an algorithm for knowledge compilation is measured by the number ofthe clauses in the result.In this paper, we propose a new reasoning rule: Strengthening Extension Rule,abbreviated as SER, and has proved the relationship between extension negativehyper resolution and negative hyper resolution. We can use SER to compile a CNFformula to an EPCCL theory, and we use SER to rewrite the KCER algorithm whichhas proposed by Minghao Yin et al. Finally, we propose IKCCER algorithm, whichuses dynamic online reasoning to reduce the space complexity enormously, and canmaintain the efficient of KCCER.Hyper extension rule is the expansion of extension rule. We can compute the unionand difference set of two sets of maximum terms which are extended by two clausesrespectively based on the hyper extension rule, and the results is saved as EPCCLtheories. In this paper, we propose extension refutation, which is a novel reasoningmethod. A link between extension refutation and knowledge compilation is alsoestablished. We also introduce two knowledge compilation methods based on hyperextension rule: the algorithm UKCHER of computing the union set and the algorithmDKCHER of calculating the difference set, which are two novel knowledgecompilation methods. UKCHER is the only one of the EPCCL compilers that can beparallelized, and the efficiency and quality of DKCHER are excellent for the difficultproblems around phase transition point. Experimental results show that, the efficiency and quality of UKCHER are all superior to the algorithm KCER proposed by Lin etal.; when the ratio of the clause number and the variable number is bigger, theefficiency and quality of DKCHER is better. DKCHER has strong competitivenesscomparing with other existing knowledge compilation algorithms of EPCCL theory.The three algorithms proposed by us in this paper improve the knowledgecompilation based on ER from different aspects. IKCCER intend to solve the problemof KCER with memory overflow. It can compile some problems which cannot bedone by KCER, since KCER is too easy to exhaust all memory. UKCHER andDKCHER are two novel algorithms for knowlecge compilation. Both of them employthe new structures, which are different from the buckets elimation emploied byKCER, to compile CNF formulae to EPCCL. So they have the different propertiesfrom KCER. DKCHER is more efficient for the SAT instances which are near thephase transition point. UKCEHR employs the incremental structure to determine thesatisfiability of the input CNF formulae in the process of compilation.