Journal of Software:2017.28(8):2096-2112

(吉林大学 计算机科学与技术学院, 吉林 长春 130012;吉林大学 计算机科学与技术学院, 吉林 长春 130012;吉林大学 数学学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012)
Knowledge Compilation Algorithm Based on Computing the Intersection for EPCCL Theories
NIU Dang-Dang,LIU Lei,LÜ Shuai
(College of Computer Science and Technology, Jilin University, Changchun 130012, China;College of Computer Science and Technology, Jilin University, Changchun 130012, China;College of Mathematics, Jilin University, Changchun 130012, China;Key Laboratory of Symbolic Computation and Knowledge Engineering(Jilin University), Ministry of Education, Changchun 130012, China)
Chart / table
Similar Articles
Article :Browse 1088   Download 718
Received:November 24, 2015    Revised:April 04, 2016
> 中文摘要: 超扩展规则是对扩展规则的扩充,基于超扩展规则能够求得任意两个非互补且不相互蕴含的子句所能扩展出极大项集的交集、差集和并集,并将所得结果以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.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61300049,61502197,61503044);教育部高等学校博士学科点专项科研基金(20120061120059);吉林省重点科技攻关项目(20130206052GX);吉林省自然科学基金(20140520069JH,20150101054JC,20150520058JH) 国家自然科学基金(61300049,61502197,61503044);教育部高等学校博士学科点专项科研基金(20120061120059);吉林省重点科技攻关项目(20130206052GX);吉林省自然科学基金(20140520069JH,20150101054JC,20150520058JH)
Foundation items: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)
Reference text:


NIU Dang-Dang,LIU Lei,LÜ Shuai.Knowledge Compilation Algorithm Based on Computing the Intersection for EPCCL Theories.Journal of Software,2017,28(8):2096-2112