A novel structure-exploiting encoding for SAT-based diagnosis

ABSTRACT

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.

KEYWORDS:

• Diagnosis
• satisfiability
• search
• abstraction

Acknowledgement

All of this work was carried out while the author was part of Riphah International University Islamabad Pakistan.

Disclosure statement

No potential conflictof interest was reported by the author(s).