Minimal Cardinality Diagnosis in Problems with Multiple Observations.

Area of Science:

• Computer Science
• Artificial Intelligence
• Systems Engineering

Background:

• Model-Based Diagnosis (MBD) is a standard technique for identifying system faults using system models.
• Diagnoses are explanations of which components are faulty, derived from observed abnormal behavior.
• Handling multiple observations, especially with intermittent faults, presents significant challenges in MBD.

Purpose of the Study:

• To develop and evaluate SAT-based approaches for Model-Based Diagnosis with multiple observations.
• To address the complexities introduced by intermittently failing components in diagnostic systems.
• To compare the efficacy of two distinct SAT-based strategies for MBD.

Main Methods:

• Formulating the MBD problem with multiple observations as a Boolean satisfiability (SAT) problem.
• Developing a first approach that compiles the entire problem into a single SAT formula.
• Developing a second approach that solves each observation independently and then integrates the results.

Main Results:

• Experimental comparison of the two SAT-based approaches on a standard diagnosis benchmark.
• Analysis of the advantages and disadvantages of each proposed method.
• Demonstration of the feasibility of using SAT solvers for complex MBD scenarios.

Conclusions:

• SAT-based methods offer a promising avenue for solving MBD with multiple observations.
• The choice between the single-formula and independent-solving approaches depends on specific system characteristics and diagnostic needs.
• Further research can refine these SAT-based techniques for improved diagnostic accuracy and efficiency.