Efficient Model-Based Diagnosis of Sequential Circuits


  • Alexander Feldman PARC Inc.
  • Ingo Pill Graz Univ. of Technology
  • Franza Wotawa Graz Univ. of Technology
  • Ion Matei PARC Inc.
  • Johan de Kleer PARC Inc.




In Model-Based Diagnosis (MBD), we concern ourselves with the health and safety of physical and software systems. Although we often use different knowledge representations and algorithms, some tools like satisfiability (SAT) solvers and temporal logics, are used in both domains. In this paper we introduce Finite Trace Next Logic (FTNL) models of sequential circuits and propose an enhanced algorithm for computing minimal-cardinality diagnoses.

Existing state-of-the-art satisfiability algorithms for minimal diagnosis use Sorting Networks (SNs) for constraining the cardinality of the diagnostic candidates. In our approach we exploit Multi-Operand Adders (MOAs). Based on extensive tests with ISCAS-89 circuits, we found that MOAs enable Conjunctive Normal Form (CNF) encodings that are significantly more compact. These encodings lead to 19.7 to 67.6 times fewer variables and 18.4 to 62 times fewer clauses. For converting an FTNL model to CNF, we could achieve a speed-up ranging from 6.2 to 22.2. Using SNs fosters 3.4 to 5.5 times faster on-line satisfiability checking though. This makes MOAs preferable for applications where RAM and off-line time are more limited than on-line CPU time.




How to Cite

Feldman, A., Pill, I., Wotawa, F., Matei, I., & de Kleer, J. (2020). Efficient Model-Based Diagnosis of Sequential Circuits. Proceedings of the AAAI Conference on Artificial Intelligence, 34(03), 2814-2821. https://doi.org/10.1609/aaai.v34i03.5670



AAAI Technical Track: Knowledge Representation and Reasoning