Knowledge Compilation Methods Based on the Clausal Relevance and Extension Rule

We introduce the concepts of Relevancematrix (RM) and Relevance-set (RS). And we construct the association between RM and the Knowledge compilation (KC) methods based on Extension rule (ER). Based on the basic parameters of RS and the relationship between RM and the KC methods based on ER, we design two efficient heuristics, called M2S (maximum sum of elements in RS and sum of literals in RS) and MNE (minimum number of maximum terms not extended by RS). Both of above heuristics intend to find the minimum set of maximum terms which cannot be extended by RS. Furthermore, we apply M2S and MNE on KCER. M2S KCER (KCER with M2S) and MNE KCER (KCER with MNE) are designed and implemented based on M2S and MNE, respectively. Experimentally, for the SAT instances with random lengths of clauses, M2S KCER and MNE KCER can improve the efficiency and quality of KCER sharply, and they are two best KC algorithms of EPCCL (each pair contains complementary literal) theory in all KC algorithms based on KCER.