本文選題：基于模型診斷 + 無(wú)解空間剪枝�。� 參考：《吉林大學(xué)》2017年碩士論文

【摘要】：基于模型診斷是一種智能診斷推理技術(shù),旨在解決第一代專(zhuān)家診斷系統(tǒng)的重大缺陷,在人工智能領(lǐng)域內(nèi)一直是熱門(mén)研究課題之一�；谀Ｐ驮\斷利用設(shè)備的內(nèi)部拓?fù)浣Y(jié)構(gòu)與觀(guān)測(cè)行為知識(shí)進(jìn)行診斷,被人工智能領(lǐng)域?qū)＜曳Q(chēng)為診斷理論和技術(shù)上面的又一革命,對(duì)整個(gè)人工智能的發(fā)展起著不可替代的推動(dòng)作用。經(jīng)過(guò)幾十年的理論發(fā)展,基于模型診斷在實(shí)際的應(yīng)用領(lǐng)域也越來(lái)越廣泛。例如醫(yī)學(xué)系統(tǒng)診斷、電路故障診斷、汽車(chē)故障診斷、大型VHDL程序的故障診斷、網(wǎng)絡(luò)通訊故障診斷等。基于模型診斷問(wèn)題的經(jīng)典求解方法包括兩階段求解過(guò)程,得到最后的診斷結(jié)果。第一步,計(jì)算極小沖突集合;第二步,根據(jù)極小沖突集求解得到極小碰集。這兩個(gè)步驟在得到診斷結(jié)果的過(guò)程中扮演中重要的作用。對(duì)于碰集問(wèn)題,主要的求解方法有基于枚舉的完備性算法和基于局部搜索的非完備性算法。隨著越來(lái)越多的學(xué)者投入到基于模型診斷問(wèn)題中,許多新的求解方法也涌現(xiàn)出來(lái)�？蓾M(mǎn)足性問(wèn)題(SAT問(wèn)題)也是人工智能領(lǐng)域中很活躍的一個(gè)分支。SAT問(wèn)題是NP-Complete問(wèn)題,將人工智能領(lǐng)域中許多NP-Complete問(wèn)題編碼成SAT問(wèn)題進(jìn)行求解是常見(jiàn)的方法。近些年以來(lái),隨著SAT求解器效率的逐漸提高,基于模型診斷問(wèn)題也被編碼成SAT問(wèn)題求解。SAT問(wèn)題使用合取范式(CNF)表示電路,所以在將基于模型診斷問(wèn)題編碼成SAT問(wèn)題的過(guò)程中,主要將邏輯門(mén)電路轉(zhuǎn)換成CNF形式的文件。在使用SAT問(wèn)題求解基于模型診斷問(wèn)題時(shí),如何結(jié)合問(wèn)題的邏輯結(jié)構(gòu)特征,給出更好的方法減少調(diào)用SAT求解器的次數(shù)成為了現(xiàn)在國(guó)內(nèi)外學(xué)者的研究熱點(diǎn)。在判斷診斷系統(tǒng)中的一個(gè)組件集合是否是系統(tǒng)的診斷時(shí),趙相福等學(xué)者提出的CSSE-Tree算法主要思想是將給定組件集合的補(bǔ)集中所有組件正常行為描述、觀(guān)測(cè)描述和系統(tǒng)描述構(gòu)造成一個(gè)CNF形式文件,然后調(diào)用SAT求解器進(jìn)行求解。在此基礎(chǔ)上,為了得到系統(tǒng)所有診斷解,CSSE-Tree算法結(jié)合集合枚舉樹(shù)模型,根據(jù)診斷系統(tǒng)中組件的個(gè)數(shù),枚舉出組件集合的所有冪集合,然后對(duì)冪集合進(jìn)行逐個(gè)判斷,求解最后的極小診斷解。但是,當(dāng)系統(tǒng)中組件個(gè)數(shù)過(guò)多的時(shí)候,組件集合的冪集合個(gè)數(shù)會(huì)變得十分龐大,因此CSSE-Tree算法利用了極小診斷解的真超集一定不是極小診斷解的剪枝策略對(duì)集合枚舉樹(shù)進(jìn)行剪枝。然而對(duì)CSSE-Tree算法進(jìn)行深入研究后,本文發(fā)現(xiàn)只對(duì)極小診斷解的子孫結(jié)點(diǎn)進(jìn)行剪枝剪掉的僅僅是少數(shù)結(jié)點(diǎn)。而在集合枚舉樹(shù)中,大量不是診斷解的結(jié)點(diǎn)仍然需要調(diào)用SAT求解器進(jìn)行判斷。針對(duì)僅對(duì)診斷解結(jié)點(diǎn)進(jìn)行剪枝的不足,本文結(jié)合診斷問(wèn)題和SAT求解過(guò)程的特征,提出了先對(duì)集合枚舉樹(shù)中包含組件個(gè)數(shù)較多的候選診斷進(jìn)行判斷的方法,從而減少求解問(wèn)題的規(guī)模。根據(jù)非診斷解的真子集一定不是診斷解的理論基礎(chǔ),首次提出了對(duì)不是診斷解的空間也進(jìn)行剪枝的策略,達(dá)到了對(duì)診斷的無(wú)解空間進(jìn)行剪枝的優(yōu)化�；赟AT求解器,結(jié)合集合枚舉樹(shù)模型,利用反向搜索以及有解無(wú)解空間剪枝策略,本文提出了基于反向搜索的有解無(wú)解空間剪枝方法LLBRS-Tree(Last Level Based Reverse Search Tree,LLBRS-Tree)。通過(guò)多方面的實(shí)驗(yàn)結(jié)果對(duì)比表明,算法LLBRS-Tree相比于算法CSSE-Tree,經(jīng)過(guò)有解無(wú)解空間剪枝,有效減少了調(diào)用SAT求解器的次數(shù),很大程度上減小了求解問(wèn)題的規(guī)模,效率得到提高。尤其在求解多診斷實(shí)例時(shí),算法LLBRS-Tree效果更加的顯著。
[Abstract]:Model based diagnosis is a kind of intelligent diagnostic reasoning technology, which aims to solve the major defects of the first generation expert diagnosis system. It is one of the hot research topics in the field of artificial intelligence. Based on the internal topology structure and the observation behavior knowledge of the equipment based on model diagnosis, it is called the diagnosis theory and the diagnosis theory by the expert of artificial intelligence. Another revolution in technology plays an irreplaceable role in the development of the whole artificial intelligence. After decades of theoretical development, model based diagnosis is becoming more and more widely used in practical applications. For example, medical system diagnosis, circuit fault diagnosis, automobile fault diagnosis, fault diagnosis of large VHDL programs, network communication failures Diagnosis and so on. The classical solution method based on the model diagnosis problem includes the two stage solution process and the final diagnosis results. The first step is to calculate the minimal conflict set; the second step is to obtain the minimal collision set according to the minimal conflict set. The two steps play an important role in the process of getting the diagnosis result. There are enumerated completeness algorithms and incompleteness algorithms based on local search. With more and more scholars put into the model based diagnosis problem, many new solutions have emerged. The satisfiability problem (SAT problem) is also a very active branch of the artificial intelligence domain.SAT problem is NP-Compl Ete problem, it is a common method to encode many NP-Complete problems in the field of artificial intelligence into SAT. In recent years, with the gradual improvement of the efficiency of the SAT solver, the model based diagnosis problem is also encoded into the SAT problem solving.SAT problem using the conjunctive paradigm (CNF) representation circuit, so it will be based on the model diagnosis problem. In the process of coding the SAT problem, the logic gate circuit is converted into a file in the form of CNF. When using the SAT problem to solve the model based diagnosis problem, how to combine the logical structure characteristics of the problem and give a better method to reduce the number of calls to the SAT solver has become the research hotspot of the scholars at home and abroad. When a set of components is the diagnosis of the system, the main idea of the CSSE-Tree algorithm proposed by Zhao Xiangfu and other scholars is to describe the normal behavior of all components of a given set of components, the observation description and the system description to be constructed into a CNF form file, and then call the SAT solver to solve it. On this basis, the system is used to obtain the system. All diagnostic solutions, CSSE-Tree algorithm combined with the set enumerated tree model, according to the number of components in the diagnostic system, enumerate all the power sets of the assembly set, and then judge the power set one by one to solve the final minimal diagnostic solution. However, when the number of components in the system is too large, the number of assembly power sets will become very Pang. So the CSSE-Tree algorithm uses the pruning strategy of the minimal diagnostic solution, which is not a minimal diagnostic solution, to prune the set enumerated tree. However, after a thorough study of the CSSE-Tree algorithm, this paper finds that only a few nodes are pruned and cut off only on the node of the minimal diagnostic solution. The node of the quantity is not the diagnostic solution still needs to call the SAT solver to judge. In view of the shortage of pruning only on the diagnosis solution node, this paper proposes a method to judge the candidate diagnosis which contains many components in the set enumeration tree, so as to reduce the scale of solving the problem by combining the diagnosis and the characteristics of the SAT solution process. According to the theory that the subsets of non diagnostic solutions are not the theoretical basis of the diagnostic solution, the strategy of pruning is proposed for the first time in the space that is not a diagnostic solution, which achieves the optimal pruning of the unsolved space for diagnosis. Based on the SAT solver, combining the set enumerated tree model, this paper uses the backward search and the unsolved space pruning strategy. LLBRS-Tree (Last Level Based Reverse Search Tree, LLBRS-Tree) based on reverse search is proposed. Through the comparison of many experimental results, it is shown that the algorithm LLBRS-Tree can effectively reduce the number of the number of SAT solvers and reduce the number of SAT solver by comparing the algorithm CSSE-Tree and the unsolved space pruning. The scale of the problem is solved and the efficiency is improved. Especially when solving multiple diagnostic instances, the algorithm LLBRS-Tree is more effective.

【學(xué)位授予單位】：吉林大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2017
【分類(lèi)號(hào)】：TP18

【參考文獻(xiàn)】

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

1 賈鳳雨;歐陽(yáng)丹彤;張立明;劉思光;;結(jié)合擴(kuò)展規(guī)則重構(gòu)的#SAT問(wèn)題增量求解方法[J];軟件學(xué)報(bào);2015年12期

2 劉娟;歐陽(yáng)丹彤;王藝源;張立明;;結(jié)合特征學(xué)習(xí)的粒子群求解極小碰集方法[J];電子學(xué)報(bào);2015年05期

3 王藝源;歐陽(yáng)丹彤;張立明;張永剛;;利用CSP求解極小碰集的方法[J];計(jì)算機(jī)研究與發(fā)展;2015年03期

4 張立明;歐陽(yáng)丹彤;曾海林;;基于動(dòng)態(tài)極大度的極小碰集求解方法[J];計(jì)算機(jī)研究與發(fā)展;2011年02期

5 趙相福;歐陽(yáng)丹彤;;使用SAT求解器產(chǎn)生所有極小沖突部件集[J];電子學(xué)報(bào);2009年04期

6 ;Deriving all minimal consistency-based diagnosis sets using SAT solvers[J];Progress in Natural Science;2009年04期

7 黃杰,陳琳,鄒鵬;一種求解極小診斷的遺傳模擬退火算法[J];軟件學(xué)報(bào);2004年09期

8 姜云飛,林笠;用布爾代數(shù)方法計(jì)算最小碰集[J];計(jì)算機(jī)學(xué)報(bào);2003年08期

相關(guān)博士學(xué)位論文 前1條

1 趙相福;離散事件系統(tǒng)基于模型診斷的若干問(wèn)題研究[D];吉林大學(xué);2009年

相關(guān)碩士學(xué)位論文 前3條

1 賈鳳雨;基于擴(kuò)展規(guī)則的模型計(jì)數(shù)方法研究[D];吉林大學(xué);2016年

2 張立明;基于一致性診斷中若干問(wèn)題研究[D];吉林大學(xué);2009年

3 趙相福;基于模型診斷中的關(guān)鍵算法研究[D];吉林大學(xué);2006年

，

本文編號(hào)：1865792