MEIR KALECH

Model-Based Diagnosis (MBD) is a well-known approach to diagnosis in medical domains. In this approach, the behavior of a system is modeled and used to identify faulty components, i.e., once a symptom of abnormal behavior is observed, an inference algorithm is run on the system model and returns possible explanations. Such explanations are referred to as diagnoses. A diagnosis is an assumption about which set of components are faulty and have caused the abnormal behavior. In this work, we focus on the case where multiple observations are available to the diagnoser, collected at different times, such that some of these observations exhibit symptoms of abnormal behavior. MBD with multiple observations is challenging because some components may fail intermittently, i.e., behave abnormally in one observation and behave normally in another, while other components may fail all the time (non-intermittently). Inspired by recent success in solving classical diagnosis problems using Boolean satisfiability (SAT) solvers, we describe two SAT-based approaches to solve this MBD with multiple observations problem. The first approach compiles the problem to a single SAT formula, and the second approach solves each observation independently and then merges them together. We compare these two approaches experimentally on a standard diagnosis benchmark and analyze their pros and cons.