主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
牛当当,刘磊,吕帅.EPCCL理论的求交知识编译算法.软件学报,2017,28(8):2096-2112
EPCCL理论的求交知识编译算法
Knowledge Compilation Algorithm Based on Computing the Intersection for EPCCL Theories
投稿时间:2015-11-24  修订日期:2016-04-04
DOI:10.13328/j.cnki.jos.005125
中文关键词:  知识编译  扩展规则  超扩展规则  EPCCL(each pair of clauses contains complementary literals)理论  并行知识编译
英文关键词:knowledge compilation  extension rule  hyper extension rule  EPCCL (each pair of clauses contains complementary literals) theory  parallel knowledge compilation
基金项目:国家自然科学基金(61300049,61502197,61503044);教育部高等学校博士学科点专项科研基金(20120061120059);吉林省重点科技攻关项目(20130206052GX);吉林省自然科学基金(20140520069JH,20150101054JC,20150520058JH)
作者单位E-mail
牛当当 吉林大学 计算机科学与技术学院, 吉林 长春 130012  
刘磊 吉林大学 计算机科学与技术学院, 吉林 长春 130012  
吕帅 吉林大学 计算机科学与技术学院, 吉林 长春 130012
吉林大学 数学学院, 吉林 长春 130012
符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012 
lus@jlu.edu.cn 
摘要点击次数: 675
全文下载次数: 509
中文摘要:
      超扩展规则是对扩展规则的扩充,基于超扩展规则能够求得任意两个非互补且不相互蕴含的子句所能扩展出极大项集的交集、差集和并集,并将所得结果以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倍.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利