EPCCL理论的求交知识编译算法
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

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


Knowledge Compilation Algorithm Based on Computing the Intersection for EPCCL Theories
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61300049, 61502197, 61503044); Specialized Research Fund for the Doctoral Program of Higher Education of China (20120061120059); Key Program for Science and Technology Development of Jilin Province of China (20130206052GX); Natural Science Research Foundation of Jilin Province of China (20140520069JH, 20150101054 JC, 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)和impP-IKCHER(IKCHER with imp-PIAE),分别采用PIAE并行合并算法和imp-PUAE并行合并算法.最后,通过实验验证了,大部分情况下,IKCHER算法的编译质量是目前为止所有EPCCL理论编译器中最优的,P-IKCHER算法所使用的合并策略并没有起到加速的效果,反而使得编译效率和编译质量有所下降;impP-IKCHER算法提高了IKCHER算法的编译效率,CPU四核环境下最高可提高2倍.

    Abstract:

    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理论的求交知识编译算法.软件学报,2017,28(8):2096-2112

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2015-11-24
  • 最后修改日期:2016-04-04
  • 录用日期:
  • 在线发布日期: 2017-08-15
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号