A Generic Model-based Diagnostic Framework using Satisfiability Solvers

Abstract: Model-based Diagnosis (MBD) can be applied in many areas such as automotive diagnostics, circuit board diagnostics, medical diagnostics, software debugging etc. A large number of studies on consistency-based MBD have adopted the features of different satisfiability solvers. The various satisfiability solvers all have their advantages and disadvantages. In this thesis project, a Generic Diagnostic Framework (GDF) is proposed based on two existing algorithms - the relational aggregation tree approach and QuickXplain. An improved algorithm is proposed, allowing the GDF to generate more complete diagnoses. Furthermore, the GDF can easily incorporate any arbitrary satisfiability solver with minimal implementation changes. The GDF has been prototyped and tested using a standard test suite. The experimental results show that GDF can solve the predefined MBD problems and provide comparable results compared to other diagnostic algorithms solving the same test suite. The improved algorithm also shows better results compared with the origina lalgorithm.