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

来源：软件学报杂志2017年第8期北京时间：

作者：牛当当,刘磊,吕帅

单位：牛当当，吉林大学 计算机科学与技术学院, 吉林 长春 13001211,刘磊，吉林大学 计算机科学与技术学院, 吉林 长春 13001202,吕帅，吉林大学 计算机科学与技术学院, 吉林 长春 130012;吉林大学 数学学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001203

摘要：超扩展规则是对扩展规则的扩充，基于超扩展规则能够求得任意两个非互补且不相互蕴含的子句所能扩展出极大项集的交集、差集和并集，并将所得结果以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）和impP-IKCHER（IKCHER with imp-PIAE），分别采用PIAE并行合并算法和imp-PUAE并行合并算法.最后，通过实验验证了，大部分情况下，IKCHER算法的编译质量是目前为止所有EPCCL理论编译器中最优的，P-IKCHER算法所使用的合并策略并没有起到加速的效果，反而使得编译效率和编译质量有所下降；impP-IKCHER算法提高了IKCHER算法的编译效率，CPU四核环境下最高可提高2倍.

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

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