Abstract:In the field of model-based diagnosis, the system description is first encoded, and all minimal conflict sets are obtained using a mature SAT solver. Finally, the minimal hitting set of the minimal conflict sets is computed as the candidate diagnosis for the equipment to be diagnosed. However, this strategy consumes a significant amount of time, as it is equivalent to solving two NP-hard problems: computing the minimal conflict set and the minimal hitting set. This study re-encodes the description of the circuit system and proposes a novel variant hitting set algorithm, HSDiag, which can directly compute the diagnosis from the encoding. Compared to state-of-the-art diagnosis algorithms that first solve conflict sets and then hitting sets, the efficiency improves by a factor of 5 to 100. As the number of circuit components increases, the encoding clauses increase linearly, while the number of diagnoses increases exponentially. Since solving all conflict sets of large-scale circuits (ISCAS-85) is impractical, the proposed HSDiag algorithm, within the same cutoff time, yields more than twice the number of solutions compared to conflict-set-based diagnosis algorithms. In addition, this study proposes an equivalence class optimization strategy, which further decomposes the conflict set by using the newly proposed set splitting rule, even if the initial conflict set is inseparable. The efficiency of the HSDiag algorithm optimized by equivalence class is improved by more than 2 times in standard Polybox and Fulladder circuits.