New Methods for Deriving All Minimal Diagnostic Using Satisfiability Algorithms

Abstract:

In the model-based diagnosis reasoning, diagnosis in two steps,they are generating all minimal conflict sets of conflict identification and Generate all the minimal hitting sets of candidate generation.In this paper, we propose new method based on SAT solver generates all minimal diagnostic.Firstly the normal behavior,system model and obtained observations are described in conjunctive normal form.,then all related clauses of Pending diagnostic system put into SAT solvers. The decision circuit failure problem is converted to satisfiability problem. Hence combine CSSE-tree for solving minimal diagnostic.It can determine the point of failure without first solving the conflict set and then with hitting set algorithm.A method is presented to directly slove the minimum fault sets,which is quite different from the traditional model-based diagnosis.The diagnosis is only finished in one step.

• Periodical: Applied Mechanics and Materials (Volumes 543-547)
• Pages: 899-903
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.543-547.899
• Online since: March 2014
• Authors: Wei Peng Zeng, Li Sha Cai*, Er Min Lin, Guo Huang
• Keywords: Circuit Fault Diagnosis, Minimal Diagnostic, MiniSAT Solver, Model-Based Diagnosis, Satisfiability, Set Enumeration Tree

References

[1] R Reiter. A theory of diagnosis from first principles[J]. Artificial Intelligence, 1987, 32(1) ：57-96.

[2] J de Kleer. Local methods for localizing faults in electroic circuits[M]. Cambridge, MA, MIT AI Mcmo, 1976, 394.

[3] Cook S A. The complexity of theorem-proving procedures[C]/Proceedings of the third ACM Symposium on Theory of Computing. 1971: 151-158.

DOI: 10.1145/800157.805047

[4] Crawford J M, Auton L D. Experimental results on the crossover point in satisfability problems[C]/Proc. of AAA193. Aug1993: 21-27.

[5] TIAN Cong, DUAN Zhenhua, WANG Xiaobing. Solving Einstein's Puzzle with SAT[J]. Computer Science, 2010, 37(5): 184-185.

[6] ZHAO Xiangfu, OUYANG Dantong. Deriving All Minimal Conflict Sets Using Satisfiability Algorithms[J]. ACTA ELECTRONICA SINICA, 2009, 37（4）：804-810.

[7] Rymon R, Search through systematic set enumeration[C]/Proceedings of the 3rd International Conference on Principles of Knowledge Representation an Reasoning. Cambridge, MA, (1992).

[8] ZHAO Xiangfu, OUYANG Dantong. New methods for deriving all minimal conflict sets in model-based diagnosis[J]. Journal of Jilin University, 2007, 37（2）：413-418.