结合结构特征反向搜索的基于模型诊断方法研究

发布时间：2018-05-09 11:11

本文选题：基于模型诊断 + 无解空间剪枝　；参考：《吉林大学》2017年硕士论文

【摘要】：基于模型诊断是一种智能诊断推理技术,旨在解决第一代专家诊断系统的重大缺陷,在人工智能领域内一直是热门研究课题之一。基于模型诊断利用设备的内部拓扑结构与观测行为知识进行诊断,被人工智能领域专家称为诊断理论和技术上面的又一革命,对整个人工智能的发展起着不可替代的推动作用。经过几十年的理论发展,基于模型诊断在实际的应用领域也越来越广泛。例如医学系统诊断、电路故障诊断、汽车故障诊断、大型VHDL程序的故障诊断、网络通讯故障诊断等。基于模型诊断问题的经典求解方法包括两阶段求解过程,得到最后的诊断结果。第一步,计算极小冲突集合;第二步,根据极小冲突集求解得到极小碰集。这两个步骤在得到诊断结果的过程中扮演中重要的作用。对于碰集问题,主要的求解方法有基于枚举的完备性算法和基于局部搜索的非完备性算法。随着越来越多的学者投入到基于模型诊断问题中,许多新的求解方法也涌现出来。可满足性问题(SAT问题)也是人工智能领域中很活跃的一个分支。SAT问题是NP-Complete问题,将人工智能领域中许多NP-Complete问题编码成SAT问题进行求解是常见的方法。近些年以来,随着SAT求解器效率的逐渐提高,基于模型诊断问题也被编码成SAT问题求解。SAT问题使用合取范式(CNF)表示电路,所以在将基于模型诊断问题编码成SAT问题的过程中,主要将逻辑门电路转换成CNF形式的文件。在使用SAT问题求解基于模型诊断问题时,如何结合问题的逻辑结构特征,给出更好的方法减少调用SAT求解器的次数成为了现在国内外学者的研究热点。在判断诊断系统中的一个组件集合是否是系统的诊断时,赵相福等学者提出的CSSE-Tree算法主要思想是将给定组件集合的补集中所有组件正常行为描述、观测描述和系统描述构造成一个CNF形式文件,然后调用SAT求解器进行求解。在此基础上,为了得到系统所有诊断解,CSSE-Tree算法结合集合枚举树模型,根据诊断系统中组件的个数,枚举出组件集合的所有幂集合,然后对幂集合进行逐个判断,求解最后的极小诊断解。但是,当系统中组件个数过多的时候,组件集合的幂集合个数会变得十分庞大,因此CSSE-Tree算法利用了极小诊断解的真超集一定不是极小诊断解的剪枝策略对集合枚举树进行剪枝。然而对CSSE-Tree算法进行深入研究后,本文发现只对极小诊断解的子孙结点进行剪枝剪掉的仅仅是少数结点。而在集合枚举树中,大量不是诊断解的结点仍然需要调用SAT求解器进行判断。针对仅对诊断解结点进行剪枝的不足,本文结合诊断问题和SAT求解过程的特征,提出了先对集合枚举树中包含组件个数较多的候选诊断进行判断的方法,从而减少求解问题的规模。根据非诊断解的真子集一定不是诊断解的理论基础,首次提出了对不是诊断解的空间也进行剪枝的策略,达到了对诊断的无解空间进行剪枝的优化。基于SAT求解器,结合集合枚举树模型,利用反向搜索以及有解无解空间剪枝策略,本文提出了基于反向搜索的有解无解空间剪枝方法LLBRS-Tree(Last Level Based Reverse Search Tree,LLBRS-Tree)。通过多方面的实验结果对比表明,算法LLBRS-Tree相比于算法CSSE-Tree,经过有解无解空间剪枝,有效减少了调用SAT求解器的次数,很大程度上减小了求解问题的规模,效率得到提高。尤其在求解多诊断实例时,算法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.

【学位授予单位】：吉林大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TP18

【参考文献】