Research On The Knowledge Compilation Methods Based On The Extension Rule

Knowledge compilation(KC)can efficiently solve repetitive reasoning tasks.And KC has been proved quite influential in a wide range of practical areas,including model checking,logic synthesis,diagnosis,product configuration,system design and automated planning.Knowledge compilation comprises a two-stage process: offline-compilation and online-reasoning.Improving the efficiency of KC can reduce the time of offline-compilation.And improving the quality of KC can reduce the time of every online-reasoning.Based on extension rule(ER),Lin et al.proposed a knowledge method KCER which compiles CNF formulae to EPCCL(each pair contains complementary literals)theories.Afterwards,many researchers focus on the researches of knowledge compilation methods for EPCCL.In this paper,we research on improving knowledge compilation methods for EPCCL based on heuristics,new compilation framework,parallel compilation,complementary knowledge compilation etc.We intend to further improve the compilation efficiency and compilation quality of EPCCL.The main research contents and innovation points of this paper are shown as below:1.We introduce the concepts of relevance-matrix(RM)and relevance-set(RS).And we construct the association between RM and the KC methods based on 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).And both of above heuristics intend to find the minimum set of maximum terms which cannot be extended by RS.Different from the existing heuristic methods,M2 S and MNE mainly consider the heuristic information in the instances with different clause length.Furthermore,we apply M2 S and MNE on KCER.Then M2 S KCER(KCER with M2S)and MNE KCER(KCER with MNE)are designed and implemented based on M2 S and MNE,respectively.Experimentally,for the SAT instances with random lengths of clauses,M2 S KCER and MNE KCER can improve the efficiency and quality of KCER sharply.2.We propose a new parallelizable knowledge compilation algorithm for EPCCL theories,IKCHER,which is based on computing the intersection of maximum terms sets.IKCHER is suitable for compiling hard SAT instances.We can compute the union set,intersection set and difference set of two sets of maximum terms which are extended by two non-complementary and non-implication clauses respectively based on the HER(hyper extension rule),and the results is saved as EPCCL theories.Based on the properties of HER,IKCHER computes the intersection of maximum terms which can not be extended by all clauses in the input CNF formula,and the computing result is saved as EPCCL theory.Then IKCHER computes the maximum terms which can not be extended by the above result based on the above method.The second computing result is an EPCCL theory which is equivalent to the input CNF formula.Experimental results show that: IKCHER has good knowledge compilation efficiency and knowledge compilation quality,and is one of the best knowledge compilation methods for EPCCL theory.3.We introduce the parallel strategies for UKCHER algorithm and IKCHER algorithm,and corresponding parallel algorithms are implemented.Parallel reasoning is an effective method for improving the efficiency of reasoning algorithms.We study on the parallel strategies of union merging and intersection merging,and propose PUAE algorithm and PIAE algorithm respectively.Combining parallelly computing union set and parallelly computing intersection set with the above two merging strategies,we introduce P-UKCHER algorithm and P-IKCHER algorithm.Through using the origin CNF formulae of EPCCL theories,another two efficient merging algorithm imp-PIAE and imp-PUAE are proposed.Then two corresponding parallel algorithms impP-IKCHER and impP-UKCHER are also proposed.Experimental results show that: When the number of CPU cores is 4,although P-UKCHER does not improve the efficiency of UKCHER,the compilation quality is improved 4 times as much in the best case;impP-UKCHER can improve the efficiency and compilation quality of UKCHER at the same time,and the compilation quality can also be improved 4 times as much in the best case;P-IKCHER algorithm does not improve the compilation quality and compilation efficiency of IKCHER;imp P-IKCHER algorithms can maintain the compilation quality of IKCHER,and improve the compilation efficiency of IKCHER twice as much in the best cases.4.We introduce the complementary KC method that is a new and non-equivalent way for KC.The concept of complementary formula(COMF)is also proposed.According to the above,we design the C2 C algorithm based on the HER.C2 C can compile each CNF formula to corresponding c-FCCD(complementary fully complementary connected diagram)which is a kind of COMF and an EPCCL.Through theoretical analysis,we prove the queries in KC map which are supported by COMF and c-FCCD in polynomial time respectively,and the transforms in KC map which are supported by EPCCL,COMF and c-FCCD in polynomial time respectively.c-FCCD can support all eight queries and two transforms in KC map in polynomial time.Different from the existing KC methods,the target languages of complementary KC are complementary formulae,and the online-reasoning is complemented based on complementary formulae.Experimentally,C2 C is competitive with the existing KC methods based on ER or HER.In summary,this paper further improves the compilation efficiency and compilation quality of KC methods for EPCCL based on heuristics,new compilation framework,parallel compilation,complementary knowledge compilation etc.,and our works can provide reference for the improvements of KC methods for other compilation languages.