知識編譯能夠提高重復性任務的求解效率,并且已經(jīng)成功被應用到模型檢測、邏輯綜合、診斷、產(chǎn)品配置、系統(tǒng)設計、自動規(guī)劃等多個領(lǐng)域。知識編譯的主要思想是將問題的求解分為兩個基本階段:離線編譯和在線推理。提高知識編譯方法的編譯效率能夠減少離線編譯所消耗的時間,而提高知識編譯方法的編譯質(zhì)量則能夠減少每次在線推理所消耗的時間。在擴展規(guī)則的基礎上,Lin等人提出了一種基于擴展規(guī)則的知識編譯方法KCER,可以將子句集編譯為EPCCL理論。隨后,許多學者針對EPCCL理論的編譯展開了深入地研究。本文基于擴展規(guī)則和超擴展規(guī)則從啟發(fā)式選擇、新型編譯框架、并行編譯、互補知識編譯等方面研究了EPCCL理論的編譯方法,旨在進一步提高擴展規(guī)則知識編譯方法的編譯效率和編譯質(zhì)量。本文的主要研究內(nèi)容和創(chuàng)新成果如下:1、提出了相關(guān)性矩陣的概念,并定義了相關(guān)集。通過分析相關(guān)集的性質(zhì),利用擴展規(guī)則在相關(guān)性矩陣和KCER算法之間建立了聯(lián)系�；谙嚓P(guān)集的基本信息以及相關(guān)性矩陣與KCER算法的聯(lián)系,本文設計了MNE啟發(fā)式和M2S啟發(fā)式,用于選擇滿足“相關(guān)集所不能擴展出的極大項集對應EPCCL理論規(guī)模較小”的子句。不同于現(xiàn)有啟發(fā)式策略,MNE啟發(fā)式和M2S啟發(fā)式主要考慮不同子句長度實例中的啟發(fā)式信息。最后,設計并實現(xiàn)了MNE_KCER算法和M2S_KCER算法。實驗結(jié)果表明:對于隨機子句長度的實例,MNE_KCER算法和M2S_KCER算法相比于KCER算法能夠大幅度降低編譯結(jié)果的規(guī)模,并且具有更高的編譯效率。2、提出了一種新的EPCCL理論編譯算法:求交知識編譯算法IKCHER,適合難解類SAT問題的知識編譯,同時是一種可并行的知識編譯算法�；诔瑪U展規(guī)則能夠求得任意兩個非互補且不相互蘊含的子句所能擴展出極大項集的交集、差集和并集,并將所得結(jié)果以EPCCL理論的形式保存。IKCHER算法基于超擴展規(guī)則,通過計算所有子句所不能擴展出極大項集的交集得出輸入子句集所不能擴展出的極大項集,并將結(jié)果保存為EPCCL理論,然后再用相同方法求得上述計算結(jié)果所不能擴展出極大項集對應的EPCCL理論,進而得出與輸入子句集等價的EPCCL理論。實驗結(jié)果表明:IKCHER算法具有較高的編譯效率和編譯質(zhì)量,是目前為止最優(yōu)秀的EPCCL理論編譯算法之一。3、提出了UKCHER算法和IKCHER算法的并行化策略,并實現(xiàn)了相關(guān)并行算法。并行推理是提高推理方法效率的有效策略�；诔瑪U展規(guī)則研究了多個EPCCL理論的并行求并合并和并行求交合并,分別提出了PUAE算法和PIAE算法。結(jié)合并行求并編譯和并行求交編譯以及上述合并策略,提出了P-UKCHER算法和P-IKCHER算法�；趯斎隕PCCL理論對應普通子句集的利用,設計了高效的并行求并算法imp-PUAE和并行求交算法imp-PIAE,以及相應的并行編譯算法impP-IKCHER和impP-UKCHER。實驗結(jié)果表明:P-UKCHER算法雖然沒有提升UKCHER算法的效率,但能夠提升UKCHER算法編譯結(jié)果的質(zhì)量,最好情況下可提升4倍;impP-UKCHER算法能夠提高UKCHER算法的效率,同時也能夠提升編譯結(jié)果的質(zhì)量,同樣最好情況下可提升4倍;P-IKCHER算法所使用的合并策略并沒有起到加速的效果,反而使得編譯效率和編譯質(zhì)量有所下降;impP-IKCHER算法提高了IKCHER算法的編譯效率,四核并行下最高可提高兩倍。4、提出了互補知識編譯方法,是一種新的非等價的知識編譯方法。提出了互補公式(COMF)的概念,并基于超擴展規(guī)則提出了C2C編譯算法。C2C能夠?qū)⑷我庾泳浼幾g為相應的c-FCCD公式。c-FCCD是一種互補公式,同時也是一種EPCCL理論。通過理論分析,證明了COMF和c-FCCD多項式時間內(nèi)所能支持的知識編譯圖譜中的查詢操作,以及COMF、c-FCCD和EPCCL理論多項式時間內(nèi)所能支持的知識編譯圖譜中的轉(zhuǎn)化操作。其中,c-FCCD能夠在多項式時間內(nèi)支持知識編譯圖譜中的全部八種查詢操作以及兩種轉(zhuǎn)化操作。不同于現(xiàn)有知識編譯方法,互補知識編譯以互補公式為編譯目標進行編譯,然后在互補公式上完成在線推理任務。實驗結(jié)果表明:相比于現(xiàn)有基于擴展規(guī)則或超擴展規(guī)則的知識編譯算法,C2C具有最優(yōu)的編譯效率和編譯質(zhì)量。綜上,本文從啟發(fā)式選擇、新型編譯框架、并行編譯、互補知識編譯等方面進一步提高了EPCCL理論編譯方法的編譯效率和編譯質(zhì)量,同時本文工作能夠為其它目標編譯語言編譯方法的優(yōu)化提供借鑒。
【學位單位】：吉林大學
【學位級別】：博士
【學位年份】：2018
【中圖分類】：TP314;TP181
【文章目錄】：
摘要
abstract
第1章 緒論
    1.1 研究背景與意義
    1.2 命題邏輯基礎
        1.2.1 命題邏輯基礎概念
        1.2.2 命題邏輯中的常見推理問題
        1.2.3 命題邏輯中的常見轉(zhuǎn)化操作
    1.3 擴展規(guī)則推理方法與知識編譯方法的研究現(xiàn)狀
        1.3.1 擴展規(guī)則推理方法的研究現(xiàn)狀
        1.3.2 知識編譯方法的研究現(xiàn)狀
        1.3.3 知識編譯目標語言的評價標準
    1.4 本文主要工作
    1.5 本文結(jié)構(gòu)安排
第2章 基于子句相關(guān)性的擴展規(guī)則知識編譯
    2.1 相關(guān)性矩陣
        2.1.1 相關(guān)性矩陣及其計算方法
        2.1.2 相關(guān)性矩陣和知識編譯的關(guān)聯(lián)關(guān)系
    2.2 基于相關(guān)性的啟發(fā)式策略
        2.2.1 M2S啟發(fā)式
        2.2.2 MNE啟發(fā)式
    2.3 實驗結(jié)果
        2.3.1 在隨機子句長度實例上的測試
        2.3.2 在固定子句長度實例上的測試
        2.3.3 與其它目標語言編譯器的對比測試
    2.4 本章小結(jié)
第3章 EPCCL理論的求交編譯方法
    3.1 超擴展規(guī)則
    3.2 求交知識編譯算法
    3.3 實驗結(jié)果
        3.3.1 在隨機子句長度實例上的測試
        3.3.2 在固定子句長度實例上的測試
    3.4 本章小結(jié)
第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 實驗結(jié)果
        4.3.1 IKCHER算法并行化的測試
        4.3.2 UKCHER算法并行化的測試
    4.4 本章小結(jié)
第5章 互補知識編譯方法
    5.1 互補公式
    5.2 CNF到c-FCCD的編譯算法
    5.3 基于CCD語言的推理方法
        5.3.1 基于CCD語言的查詢操作
        5.3.2 基于CCD語言的轉(zhuǎn)化操作
    5.4 實驗結(jié)果
    5.5 本章小結(jié)
第6章 總結(jié)與展望
    6.1 總結(jié)
    6.2 未來工作展望
參考文獻
攻讀博士期間發(fā)表的學術(shù)論文及參與的科研項目
致謝

【參考文獻】

相關(guān)期刊論文 前7條

1 楊洋;劉磊;李廣力;張桐搏;呂帥;;一種新的基于局部搜索的擴展規(guī)則推理方法[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 賈鳳雨;歐陽丹彤;張立明;劉思光;;結(jié)合擴展規(guī)則重構(gòu)的#SAT問題增量求解方法[J];軟件學報;2015年12期

5 劉磊;牛當當;李壯;呂帥;;基于超擴展規(guī)則的動態(tài)在線推理算法[J];哈爾濱工程大學學報;2015年12期

6 張立明;歐陽丹彤;趙毅;;半擴展規(guī)則下分解的定理證明方法[J];軟件學報;2015年09期

7 劉磊;牛當當;呂帥;;基于超擴展規(guī)則的知識編譯方法[J];計算機學報;2016年08期

本文編號：2883074