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

作     者：牛当当 刘磊 吕帅 NIU Dang-Dang;LIU Lei;L(U) Shuai

作者机构：吉林大学计算机科学与技术学院吉林长春130012 吉林大学数学学院吉林长春130012 符号计算与知识工程教育部重点实验室(吉林大学)吉林长春130012 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2017年第28卷第8期

页      面：2096-2112页

核心收录：

学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 081104[工学-模式识别与智能系统] 08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

主　　题：知识编译 扩展规则 超扩展规则 EPCCL(each pair of clauses contains complementary literals)理论 并行知识编译 

摘      要：超扩展规则是对扩展规则的扩充,基于超扩展规则能够求得任意两个非互补且不相互蕴含的子句所能扩展出极大项集的交集、差集和并集,并将所得结果以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倍.