Knowledge Compilation Methods Based on the Clausal Relevance and Extension Rule  

作　　者：NIU Dangdang LIU Lei LYU Shuai 

机构地区：[1]College of Computer Science and Technology,Jilin University [2]Key Laboratory of Symbolic Computation and Knowledge Engineering (Jilin University),Ministry of Education

出　　处：《Chinese Journal of Electronics》2018年第5期1037-1042,共6页电子学报（英文版）

基　　金：supported by the National Natural Science Foundation of China(No.61300049,No.61502197,No.61503044,No.61763003);the Natural Science Research Foundation of Jilin Province of China(No.20180101053JC)

摘　　要：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.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.

关 键 词：Extension rule Knowledge compilation Clausal relevance Heuristic strategy 

分 类 号：TP182[自动化与计算机技术—控制理论与控制工程]