命題可滿足問題（propositional satisfiability problem,SAT）是人工智能領域的研究熱點,也是數(shù)理邏輯及計算機研究中的核心問題,對人工智能發(fā)展起到了非常重要的推動作用。命題可滿足問題擅長將一些艱難的故障求解轉化為問題系統(tǒng)中命題公式是否存在可滿足賦值的問題,并給出故障識別。極小不可滿足集（minimal unsatisfiable subset,MUS）問題是命題可滿足問題的擴展問題。在求解極小不可滿足解時,通常將不可滿足性問題轉換為命題可滿足問題,利用SAT求解器來給出是否一致可滿足的判定。目前求解極小不可滿足集效率較高的兩種遍歷結構為哈斯圖和枚舉樹。哈斯圖結構主要是利用圖的邏輯結構構建節(jié)點之間的聯(lián)系,適用于廣泛的約束關系處理。圖結構主要應用于關系規(guī)范調試、不一致檢測、模型驗證等問題中。極小沖突問題是極小不可滿足問題在基于模型診斷上的應用,主要采用枚舉樹結構,利用樹的特性對電路系統(tǒng)中元件集的全枚舉進行遍歷。相對于圖結構遍歷,樹結構遍歷求解極小沖突問題節(jié)點跳轉方便,配合剪枝策略剪去枚舉樹中不需要遍歷的節(jié)點使求解效率更快。在基于圖結構求解方法中,MARCO... 

【文章來源】：吉林大學吉林省 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：55 頁

【學位級別】：碩士

【文章目錄】：
摘要
abstract
第1章 緒論
    1.1 研究背景和意義
    1.2 研究現(xiàn)狀
    1.3 本文工作
第2章 極小不可滿足問題
    2.1 SAT相關概念
    2.2 極小不可滿足集
    2.3 遍歷結構
        2.3.1 圖結構求解極小不可滿足問題
        2.3.2 樹結構求解極小沖突集問題
    2.4 本章小結
第3章 基于雙模型的MUS求解方法
    3.1 相關定義
    3.2 基于極大化模型的MARCO方法
    3.3 基于雙模型的MARCO-MAM方法
    3.4 實例對比分析
    3.5 實驗結果及分析
    3.6 本章小結
第4章 結合故障邏輯關系的極小沖突集求解方法
    4.1 相關定義
    4.2 結合故障輸出的MCS-SFFO方法
    4.3 結合故障輸出邏輯結構的MCS-FLR方法
    4.4 MCS-FLR算法分析
    4.5 實例對比分析
    4.6 實驗結果與分析
    4.7 本章小結
第5章 總結與展望
    5.1 工作總結
    5.2 工作展望
參考文獻
作者簡介及在學期間所取得的科研成果
致謝


【參考文獻】：
期刊論文
[1]基于子集一致性檢測的診斷解極小性判定方法[J]. 田乃予,歐陽丹彤,劉夢,張立明.  計算機研究與發(fā)展. 2019(07)
[2]結合故障輸出結構特征的極小沖突求解算法[J]. 徐旖旎,歐陽丹彤,劉夢,張立明,張永剛.  計算機研究與發(fā)展. 2018(11)
[3]Efficient zonal diagnosis with maximum satisfiability[J]. Meng LIU,Dantong OUYANG,Shaowei CAI,Liming ZHANG.  Science China（Information Sciences）. 2018(11)
[4]結合問題特征的分組式診斷方法[J]. 劉夢,歐陽丹彤,劉伯文,張立明,張永剛.  電子學報. 2018(03)
[5]結合問題特征利用SE-Tree反向深度求解沖突集的方法[J]. 歐陽丹彤,劉伯文,周建華,張立明.  電子學報. 2017(05)
[6]基于模型診斷中結合問題特征的新方法[J]. 歐陽丹彤,周建華,劉伯文,張立明.  計算機研究與發(fā)展. 2017(03)
[7]結合SE-Tree結構特征的極小碰集求解算法[J]. 劉思光,歐陽丹彤,王藝源,賈鳳雨,張立明.  計算機研究與發(fā)展. 2016(11)
[8]使用SAT求解器產生所有極小沖突部件集[J]. 趙相福,歐陽丹彤.  電子學報. 2009(04)
[9]一種基于ATMS的求解所有極小沖突集的新方法[J]. 張立明,歐陽丹彤,趙相福.  計算機工程與科學. 2007(11)
[10]A method of combining SE-tree to compute all minimal hitting sets[J]. ZHAO Xiangfu and OUYANG Dantong (School of Computer Science and Technology, Jilin University, Changchun 130012, China; Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education, Changchun 130012, China).  Progress in Natural Science. 2006(02)



本文編號：3585001