Knowledge Compilation Using Extension Rule Based on MCN and MO Heuristic Strategies

The key idea of theorem proving using extension rule is to use the inverse of resolution and the inclusionexclusion principle to circumvent the problem of space complexity. Knowledge compilation using extension rule, called KCER, is a new method for knowledge compilation, in which both the compilation and the querying are based on the extension rule. So KCER can be considered as a counterpart of other existing methods for knowledge compilation. After deep research on the method, two heuristic strategies MCN and MO are proposed. They utilize the information contained in the set of clauses to choose respectively relevant clauses and variables, in order to reduce the times of using extension rule, and further decrease the size of the compiled knowledge base. Furthermore, we apply MCN, MO and both of them to KCER, respectively. The algorithms MCN_KCER, MO_KCER and MCN_MO_KCER, are designed and implemented. Experimental results indicate that the MCN and MO play a great role in minimizing the size of the compiled knowledge base. When MCN and MO are used together, the efficiency becomes better. The sizes gained by MCN_MO_KCER are 1/3—1/39 times larger the sizes gained by knowledge compilation using extension rule without any heuristic strategy. Consequently, the efficiency will be advanced largely in the online reasoning phase.