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

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

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

【學(xué)位級(jí)別】：碩士

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


【參考文獻(xiàn)】：
期刊論文
[1]基于子集一致性檢測的診斷解極小性判定方法[J]. 田乃予,歐陽丹彤,劉夢,張立明.  計(jì)算機(jī)研究與發(fā)展. 2019(07)
[2]結(jié)合故障輸出結(jié)構(gòu)特征的極小沖突求解算法[J]. 徐旖旎,歐陽丹彤,劉夢,張立明,張永剛.  計(jì)算機(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]結(jié)合問題特征的分組式診斷方法[J]. 劉夢,歐陽丹彤,劉伯文,張立明,張永剛.  電子學(xué)報(bào). 2018(03)
[5]結(jié)合問題特征利用SE-Tree反向深度求解沖突集的方法[J]. 歐陽丹彤,劉伯文,周建華,張立明.  電子學(xué)報(bào). 2017(05)
[6]基于模型診斷中結(jié)合問題特征的新方法[J]. 歐陽丹彤,周建華,劉伯文,張立明.  計(jì)算機(jī)研究與發(fā)展. 2017(03)
[7]結(jié)合SE-Tree結(jié)構(gòu)特征的極小碰集求解算法[J]. 劉思光,歐陽丹彤,王藝源,賈鳳雨,張立明.  計(jì)算機(jī)研究與發(fā)展. 2016(11)
[8]使用SAT求解器產(chǎn)生所有極小沖突部件集[J]. 趙相福,歐陽丹彤.  電子學(xué)報(bào). 2009(04)
[9]一種基于ATMS的求解所有極小沖突集的新方法[J]. 張立明,歐陽丹彤,趙相福.  計(jì)算機(jī)工程與科學(xué). 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)



本文編號(hào)：3585001