When a circuit exhibits abnormal behaviour, a diagnosis of the circuit is a set of gates whose failure explains the abnormality. The cardinality of a diagnosis is the number of gates assumed to be failing. A diagnosis is of minimum cardinality if no other diagnosis of the circuit exists that has a smaller cardinality. In general, the number of diagnoses can be exponentially large, and often only a preferred set of minimum-cardinality diagnoses is computed. In propositional satisfiability (SAT), given a propositional circuit, the task is to check whether all gates of the circuit can be assigned values in a consistent manner. In SAT-based diagnosis approach, the given circuit is injected with additional circuitry modelling the health of gates as well as the cardinality constraint. Under an abnormal observation the SAT solver repeatedly computes consistent assignments to all gates in the augmented circuit where each such assignment corresponds to a minimum-cardinality diagnosis. However, diagnosis of large size circuits as well as diagnostic cases with large minimum cardinalities pose a challenge for SAT solvers. To scale diagnosis to larger and harder cases, we propose a novel encoding that captures the hierarchical structure of the circuit in terms of single-output self-contained sub-circuits called cones. Cones have been exploited in diagnostic reasoning in the past; however, our encoding is the first of its kind in a SAT-based approach. Previously, cones were used to take the abstraction of a circuit and simplify it, while we exploit cones to improve the speed and efficiency of the SAT solver. Experiments on 1800 diagnostic cases of ISCAS-85 benchmark circuits show that the new encoding allows faster and more scalable diagnosis solving 1700 cases which is 163 more than the number of cases solved by the baseline approach.

In satisfiability (SAT) the task is to determine whether a propositional formula can evaluate to true under some assignment to its variables. The formula is either represented in CNF or in circuit form. Solvers are available for both representations with comparable performance. CNF-based approach, being simpler in encoding and solver design, is more popular, in which a circuit is translated into CNF and then solved. Translation to CNF, however, increases the size of the encoding, and is not practical for some constraints such as the cardinality constraint. Circuit-based approach lacks simplicity of implementation; however, circuit representation remains compact in size and also captures problem structure where domain-specific knowledge can be exploited. An important application of SAT solving is in the area of model-based diagnosis. Our contribution in this paper is twofold enhancing the state-of-the-art in SAT solving as well as model-based diagnosis. To simplify and encourage development in circuit-based approach, we propose a new solver which can be extended with minimal effort. The solver which has been built using object-oriented paradigm allows adding a new gate by simply inheriting from existing classes and overriding some functions, hiding great deal of complexity. Then, we demonstrate its effectiveness on the problem of computing minimum-cardinality diagnoses using ISCAS-85 circuit benchmarks. We show that the new solver can solve 28 more (out of 1000) cases than its CNF-based counterpart.

When a system behaves abnormally, sequential diagnosis takes a sequence of measurements of the system until the faults causing the abnormality are identified, and the goal is to reduce the diagnostic cost, defined here as the number of measurements. To propose measurement points, previous work employs a heuristic based on reducing the entropy over a computed set of diagnoses. This approach generally has good performance in terms of diagnostic cost, but can fail to diagnose large systems when the set of diagnoses is too large. Focusing on a smaller set of probable diagnoses scales the approach but generally leads to increased average diagnostic costs. In this paper, we propose a new diagnostic framework employing four new techniques, which scales to much larger systems with good performance in terms of diagnostic cost. First, we propose a new heuristic for measurement point selection that can be computed efficiently, without requiring the set of diagnoses, once the system is modeled as a Bayesian network and compiled into a logical form known as d-DNNF. Second, we extend hierarchical diagnosis, a technique based on system abstraction from our previous work, to handle probabilities so that it can be applied to sequential diagnosis to allow larger systems to be diagnosed. Third, for the largest systems where even hierarchical diagnosis fails, we propose a novel method that converts the system into one that has a smaller abstraction and whose diagnoses form a superset of those of the original system; the new system can then be diagnosed and the result mapped back to the original system. Finally, we propose a novel cost estimation function which can be used to choose an abstraction of the system that is more likely to provide optimal average cost. Experiments with ISCAS-85 benchmark circuits indicate that our approach scales to all circuits in the suite except one that has a flat structure not susceptible to useful abstraction.