Solving Strong-Fault Diagnostic Models by Model Relaxation

In Model-Based Diagnosis (MBD), the problem of computing a diagnosis in a strong-fault model (SFM) is computationally much harder than in a weak-fault model (WFM). For example, in propositional Horn models, computing the first minimal diagnosis in a weak-fault model (WFM) is in P but is NP-hard for strong-fault models. As a result, SFM problems of practical significance have not been studied in great depth within the MBD community. In this paper we describe an algorithm that renders the problem of computing a diagnosis in several important SFM subclasses no harder than a similar computation in a WFM. We propose an approach for efficiently computing minimal diagnoses for these subclasses of SFM that extends existing conflict-based algorithms like GDE (Sherlock) and CDA*. Experiments on ISCAS85 combinational circuits show (1) inference speedups with CDA* of up to a factor of 8, and (2) an average of 28% reduction in the average conflict size, at the price of an extra low-polynomial-time consistency check for a candidate diagnosis.