超扩展规则是对扩展规则的扩充,基于超扩展规则能够求得任意两个非互补且不相互蕴含的子句所能扩展出极大项集的交集、差集和并集,并将所得结果以EPCCL(each pair of clauses contains complementary literals)理论的形式保存.基于超扩展规则的性质,提出一种EPCCL理论编译算法:求交知识编译算法IKCHER(intersectionapproach 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)理论、并行知识编译
28
TP182(自动化基础理论)
国家自然科学基金61300049,61502197,61503044;教育部高等学校博士学科点专项科研基金20120061120059;吉林省重点科技攻关项目20130206052GX;吉林省自然科学基金20140520069JH,20150101054JC,20150520058JHNational Natural Science Foundation of China61300049,61502197,61503044;Specialized Research Fund for the Doctoral Program of Higher Education of China20120061120059;Key Program for Science and Technology Development of Jilin Province of China20130206052GX;Natural Science Research Foundation of Jilin Province of China20140520069JH,20150101054JC,20150520058JH