Computing Minimum-Cardinality Diagnoses Using OBDDs

The paper addresses the problem of solving diagnostic problems by exploiting OBDDs (Ordered Binary Decision Diagrams) as a way for compactly representing the set of alternative diagnoses. In the MBD (Model Based Diagnosis) community it is indeed well known that the number of diagnoses can be exponential in the system size even whenrestricted to preferred diagnoses (e.g. minimal diagnoses). In particular, the paper presents methods and heuristics for efficiently encoding the domain theory of the system model in terms of an OBDD. Such heuristics suggest suitable ordering of the OBDD variables which prevents the explosion of the OBDD size for some classes of domain theories. Moreover, we describe how to solve specific diagnostic problems represented as OBDDs and report some results on the computational complexity of such process. Finally, we introduce a mechanism for extracting diagnoses with the minimum number of faults from the OBDD which represents the entire space of diagnoses. Experimental results are collected and reported on a model representing a simplified propulsion subsystem of a spacecraft.