EPCCL理论的求交知识编译算法  

Knowledge Compilation Algorithm Based on Computing the Intersection for EPCCL Theories

作　　者：牛当当 刘磊[1] 吕帅[1,2,3] 

机构地区：[1]吉林大学计算机科学与技术学院,吉林长春130012 [2]吉林大学数学学院,吉林长春130012 [3]符号计算与知识工程教育部重点实验室(吉林大学),吉林长春130012

出　　处：《软件学报》2017年第8期2096-2112,共17页Journal of Software

基　　金：国家自然科学基金(61300049;61502197;61503044);教育部高等学校博士学科点专项科研基金(20120061120059);吉林省重点科技攻关项目(20130206052GX);吉林省自然科学基金(20140520069JH;20150101054JC;20150520058JH)~~

摘　　要：超扩展规则是对扩展规则的扩充,基于超扩展规则能够求得任意两个非互补且不相互蕴含的子句所能扩展出极大项集的交集、差集和并集,并将所得结果以EPCCL(each pair of clauses contains complementary literals)理论的形式保存.基于超扩展规则的性质,提出一种EPCCL理论编译算法:求交知识编译算法IKCHER(intersection approach to knowledge compilation based on hyper extension rule).该算法适合难解类SAT问题的知识编译,也是一种可并行的知识编译算法.研究了如何实现多个EPCCL理论的求交操作,证明了EPCCL理论的求交过程是可并行执行的,并设计了相应的并行求交算法PIAE(parellel intersection of any number of EPCCL).通过对输入EPCCL理论对应普通子句集的利用,设计了一种高效的并行求交算法imp-PIAE(improvement of PIAE).基于上述算法,还设计了两种并行知识编译算法P-IKCHER(IKCHER with PIAE)和imp P-IKCHER(IKCHER with imp-PIAE),分别采用PIAE并行合并算法和imp-PUAE并行合并算法.最后,通过实验验证了,大部分情况下,IKCHER算法的编译质量是目前为止所有EPCCL理论编译器中最优的,P-IKCHER算法所使用的合并策略并没有起到加速的效果,反而使得编译效率和编译质量有所下降;imp P-IKCHER算法提高了IKCHER算法的编译效率,CPU四核环境下最高可提高2倍.HER （hyper extension rule） is an expansion of ER （extension rule）. The results of computing the union and difference set of two sets of maximum terms which are extended by two clauses respectively based on the hyper extension rule can be saved as EPCCL （each pair of clauses contains complementary literals） theories. In this paper, a parallelizable knowledge compilation algorithm for EPCCL theories, IKCHER, is proposed based on computing the intersection of maximum terms sets. The focus is placed on the research of parallel computing the intersection sets of multiple EPCCL theories based on HER, resulting in the design of the corresponding algorithm, PIAE （parallel intersection of any number of EPCCL）. Through using the origin CNF formulae of EPCCL theories, another efficient merging algorithm imp-PIAE is proposed. Based on above methods two parallel knowledge compilation algorithms P-IKCHER and impP-IKCHER are constructed for EPCCL theories, utilizing the PIAE algorithm and imp-PIAE algorithm to merge multiple EPCCL theories respectively. Experimental results show that IKCHER algorithm has the best compilation quality of all EPCCL compilation algorithms. P-IKCHER algorithm does not improve the compilation quality and compilation efficiency of IKCHER while impP-IKCHER algorithms can maintain the compilation quality of IKCHER, and improve the compilation efficiency of IKCHER. When the number of CPU cores is 4, the compilation efficiency of IKCHER can be improved twice as much in the best cases.

关 键 词：知识编译 扩展规则 超扩展规则 EPCCL(each pair of CLAUSES CONTAINS COMPLEMENTARY literals)理论 并行知识编译 

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