基于扩展规则的知识编译方法研究

发布时间：2020-11-14 04:26

　　 知识编译能够提高重复性任务的求解效率,并且已经成功被应用到模型检测、逻辑综合、诊断、产品配置、系统设计、自动规划等多个领域。知识编译的主要思想是将问题的求解分为两个基本阶段:离线编译和在线推理。提高知识编译方法的编译效率能够减少离线编译所消耗的时间,而提高知识编译方法的编译质量则能够减少每次在线推理所消耗的时间。在扩展规则的基础上,Lin等人提出了一种基于扩展规则的知识编译方法KCER,可以将子句集编译为EPCCL理论。随后,许多学者针对EPCCL理论的编译展开了深入地研究。本文基于扩展规则和超扩展规则从启发式选择、新型编译框架、并行编译、互补知识编译等方面研究了EPCCL理论的编译方法,旨在进一步提高扩展规则知识编译方法的编译效率和编译质量。本文的主要研究内容和创新成果如下:1、提出了相关性矩阵的概念,并定义了相关集。通过分析相关集的性质,利用扩展规则在相关性矩阵和KCER算法之间建立了联系。基于相关集的基本信息以及相关性矩阵与KCER算法的联系,本文设计了MNE启发式和M2S启发式,用于选择满足“相关集所不能扩展出的极大项集对应EPCCL理论规模较小”的子句。不同于现有启发式策略,MNE启发式和M2S启发式主要考虑不同子句长度实例中的启发式信息。最后,设计并实现了MNE_KCER算法和M2S_KCER算法。实验结果表明:对于随机子句长度的实例,MNE_KCER算法和M2S_KCER算法相比于KCER算法能够大幅度降低编译结果的规模,并且具有更高的编译效率。2、提出了一种新的EPCCL理论编译算法:求交知识编译算法IKCHER,适合难解类SAT问题的知识编译,同时是一种可并行的知识编译算法。基于超扩展规则能够求得任意两个非互补且不相互蕴含的子句所能扩展出极大项集的交集、差集和并集,并将所得结果以EPCCL理论的形式保存。IKCHER算法基于超扩展规则,通过计算所有子句所不能扩展出极大项集的交集得出输入子句集所不能扩展出的极大项集,并将结果保存为EPCCL理论,然后再用相同方法求得上述计算结果所不能扩展出极大项集对应的EPCCL理论,进而得出与输入子句集等价的EPCCL理论。实验结果表明:IKCHER算法具有较高的编译效率和编译质量,是目前为止最优秀的EPCCL理论编译算法之一。3、提出了UKCHER算法和IKCHER算法的并行化策略,并实现了相关并行算法。并行推理是提高推理方法效率的有效策略。基于超扩展规则研究了多个EPCCL理论的并行求并合并和并行求交合并,分别提出了PUAE算法和PIAE算法。结合并行求并编译和并行求交编译以及上述合并策略,提出了P-UKCHER算法和P-IKCHER算法。基于对输入EPCCL理论对应普通子句集的利用,设计了高效的并行求并算法imp-PUAE和并行求交算法imp-PIAE,以及相应的并行编译算法impP-IKCHER和impP-UKCHER。实验结果表明:P-UKCHER算法虽然没有提升UKCHER算法的效率,但能够提升UKCHER算法编译结果的质量,最好情况下可提升4倍;impP-UKCHER算法能够提高UKCHER算法的效率,同时也能够提升编译结果的质量,同样最好情况下可提升4倍;P-IKCHER算法所使用的合并策略并没有起到加速的效果,反而使得编译效率和编译质量有所下降;impP-IKCHER算法提高了IKCHER算法的编译效率,四核并行下最高可提高两倍。4、提出了互补知识编译方法,是一种新的非等价的知识编译方法。提出了互补公式(COMF)的概念,并基于超扩展规则提出了C2C编译算法。C2C能够将任意子句集编译为相应的c-FCCD公式。c-FCCD是一种互补公式,同时也是一种EPCCL理论。通过理论分析,证明了COMF和c-FCCD多项式时间内所能支持的知识编译图谱中的查询操作,以及COMF、c-FCCD和EPCCL理论多项式时间内所能支持的知识编译图谱中的转化操作。其中,c-FCCD能够在多项式时间内支持知识编译图谱中的全部八种查询操作以及两种转化操作。不同于现有知识编译方法,互补知识编译以互补公式为编译目标进行编译,然后在互补公式上完成在线推理任务。实验结果表明:相比于现有基于扩展规则或超扩展规则的知识编译算法,C2C具有最优的编译效率和编译质量。综上,本文从启发式选择、新型编译框架、并行编译、互补知识编译等方面进一步提高了EPCCL理论编译方法的编译效率和编译质量,同时本文工作能够为其它目标编译语言编译方法的优化提供借鉴。
【学位单位】：吉林大学
【学位级别】：博士
【学位年份】：2018
【中图分类】：TP314;TP181
【文章目录】：
摘要
abstract
第1章 绪论
    1.1 研究背景与意义
    1.2 命题逻辑基础
        1.2.1 命题逻辑基础概念
        1.2.2 命题逻辑中的常见推理问题
        1.2.3 命题逻辑中的常见转化操作
    1.3 扩展规则推理方法与知识编译方法的研究现状
        1.3.1 扩展规则推理方法的研究现状
        1.3.2 知识编译方法的研究现状
        1.3.3 知识编译目标语言的评价标准
    1.4 本文主要工作
    1.5 本文结构安排
第2章 基于子句相关性的扩展规则知识编译
    2.1 相关性矩阵
        2.1.1 相关性矩阵及其计算方法
        2.1.2 相关性矩阵和知识编译的关联关系
    2.2 基于相关性的启发式策略
        2.2.1 M2S启发式
        2.2.2 MNE启发式
    2.3 实验结果
        2.3.1 在随机子句长度实例上的测试
        2.3.2 在固定子句长度实例上的测试
        2.3.3 与其它目标语言编译器的对比测试
    2.4 本章小结
第3章 EPCCL理论的求交编译方法
    3.1 超扩展规则
    3.2 求交知识编译算法
    3.3 实验结果
        3.3.1 在随机子句长度实例上的测试
        3.3.2 在固定子句长度实例上的测试
    3.4 本章小结
第4章 EPCCL理论的并行编译方法
    4.1 EPCCL理论的并行求交编译算法
        4.1.1 EPCCL理论的求交操作
        4.1.2 IKCHER算法的并行化
    4.2 EPCCL理论的并行求并编译算法
        4.2.1 EPCCL理论的求并操作
        4.2.2 UKCHER算法的并行化
    4.3 实验结果
        4.3.1 IKCHER算法并行化的测试
        4.3.2 UKCHER算法并行化的测试
    4.4 本章小结
第5章 互补知识编译方法
    5.1 互补公式
    5.2 CNF到c-FCCD的编译算法
    5.3 基于CCD语言的推理方法
        5.3.1 基于CCD语言的查询操作
        5.3.2 基于CCD语言的转化操作
    5.4 实验结果
    5.5 本章小结
第6章 总结与展望
    6.1 总结
    6.2 未来工作展望
参考文献
攻读博士期间发表的学术论文及参与的科研项目
致谢

【参考文献】

相关期刊论文 前7条

1 杨洋;刘磊;李广力;张桐搏;吕帅;;一种新的基于局部搜索的扩展规则推理方法[J];计算机学报;2018年04期

2 牛当当;刘磊;吕帅;;EPCCL理论的求交知识编译算法[J];软件学报;2017年08期

3 HUANG Yufang;XIAO Jianhua;JIANG Keqin;CHEN Zhihua;;Parallel Solution for Maximum Independent Set Problem by Programmable Tile Assembly[J];Chinese Journal of Electronics;2016年02期

4 贾凤雨;欧阳丹彤;张立明;刘思光;;结合扩展规则重构的#SAT问题增量求解方法[J];软件学报;2015年12期

5 刘磊;牛当当;李壮;吕帅;;基于超扩展规则的动态在线推理算法[J];哈尔滨工程大学学报;2015年12期

6 张立明;欧阳丹彤;赵毅;;半扩展规则下分解的定理证明方法[J];软件学报;2015年09期

7 刘磊;牛当当;吕帅;;基于超扩展规则的知识编译方法[J];计算机学报;2016年08期

本文编号：2883074