Deriving all minimal consistency-based diagnosis sets using SAT solvers |
| |
Authors: | Xiangfu Zhao Liming Zhang Dantong Ouyang Yu Jiao |
| |
Institution: | Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education,Jilin University,Changchun 130012,China;School of Computer Science and Technology,Jilin University,Changchun 130012,China |
| |
Abstract: | In this paper,a novel method is proposed for judging whether a component set is a consistency-based diagnostic set,using SAT solvers.Firstly,the model of the system to be diagnosed and all the observations are described with conjunctive normal forms (CNF).Then,all the related clauses in the CNF files to the components other than the considered ones are extracted,to be used for satisfiability checking by SAT solvers.Next,all the minimal consistency-based diagnostic sets are derived by the CSSE-tree or by other similar algorithms.We have implemented four related algorithms,by calling the gold medal SAT solver in SAT07 competition - RSAT.Experimental results show that all the minimal consistency-based diagnostic sets can be quickly computed.Especially our CSSE-tree has the best efficiency for the single-or double-fault diagnosis. |
| |
Keywords: | Conjunctive normal form Consistency-based diagnosis Model-based diagnosis SAT solver |
本文献已被 维普 万方数据 ScienceDirect 等数据库收录! |
| 点击此处可从《自然科学进展(英文版)》浏览原始摘要信息 |
| 点击此处可从《自然科学进展(英文版)》下载免费的PDF全文 |