Towards preferred diagnoses through local search MaxSAT

Abstract

Model-based diagnosis (MBD) is a principled approach for identifying the possible causes of unexpected behavior caused by system malfunctions and is crucial for enhancing the reliability of modern intelligent systems. Previous MBD methods often generate numerous candidate diagnoses without ensuring their accuracy in identifying fault components. In this paper, we introduce a novel Enhanced Model-Based Diagnosis (EMBD) method, which iteratively refines candidate component sets through iterative applications of our fault localization model and our proposed local search MaxSAT algorithm, achieving precise identification of faulty components. Firstly, we establish a formal fault localization model using Weighted Conjunctive Normal Form (WCNF). The model encodes the fault localization problem into a MaxSAT problem by duplicating the original circuit and inserting XOR gates between corresponding gate pairs to enable output comparison and discrepancy detection. Secondly, building upon this model, we develop NuFPS, a local search MaxSAT algorithm that identifies the maximum number of components with output logic variations across different observations, effectively pruning fault-free components from the candidate diagnoses. Experimental evaluations demonstrate that EMBD achieves significantly more accurate candidate diagnoses. Compared with state-of-the-art methods such as HSD, CMMO, DiagDO, and DPDN, EMBD achieves significant improvements, with 673.6%, 254.2%, 211.5%, and 283.2% increase in diagnosis performance, respectively.

Graphical abstract

Keywords

fault diagnosis / model-based diagnosis / fault localization model / local search / maximum satisfiability

References

[1] Reiter R . A theory of diagnosis from first principles. Artificial Intelligence, 1987, 32( 1): 57–95

[2] Moness M, Gaber L, Hussein A I, Ali H M . Automated design error debugging of digital VLSI circuits. Journal of Electronic Testing, 2022, 38( 4): 395–417

[3] Li D, Lin Y, Huang H. Ontology inconsistent problem on model-based diagnosis. In: Proceeding of the 3rd International Conference on Biomedical Engineering and Informatics. 2010, 2927−2931

[4] Ardissono L, Console L, Goy A, Petrone G, Picardi C, Segnan M, Theseider Dupre’ D. Cooperative model-based diagnosis of web services. In: Proceedings of the 16th International Workshop on Principles of Diagnosis. 2005, 125−130

[5] Torlak E, Chang F S H, Jackson D. Finding minimal unsatisfiable cores of declarative specifications. In: Proceedings of the 15th International Symposium on Formal Methods. 2008, 326−341

[6] Jannach D, Schmitz T . Model-based diagnosis of spreadsheet programs: a constraint-based debugging approach. Automated Software Engineering, 2016, 23( 1): 105–144

[7] Rodler P . Memory-limited model-based diagnosis. Artificial Intelligence, 2022, 305: 103681

[8] Dressler O, Struss P. The consistency-based approach to automated diagnosis of devices. In: Proceedings of the Principles of Knowledge Representation. 1997, 267−311

[9] Siddiqi S. Computing minimum-cardinality diagnoses by model relaxation. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence. 2011, 1087−1092

[10] Torasso P, Torta G. Computing minimum-cardinality diagnoses using OBDDs. In: Proceeding of the 26th Annual Conference on Artificial Intelligence. 2003, 224−238

[11] Biteus J, Nyberg M, Frisk E . An algorithm for computing the diagnoses with minimal cardinality in a distributed system. Engineering Applications of Artificial Intelligence, 2008, 21( 2): 269–276

[12] Zhao X, Lamperti G, Ouyang D, Tong X . Minimal diagnosis and diagnosability of discrete-event systems modeled by automata. Complexity, 2020, 2020: 4306261

[13] De Kleer J, Mackworth A K, Reiter R. Characterizing diagnoses and systems. Artificial Intelligence, 1992, 56(2−3): 197−222

[14] Armstrong D B. On finding a nearly minimal set of fault detection tests for combinational logic nets. IEEE Transactions on Electronic Computers, 1966, EC-15(1): 66−73

[15] Rodler P . DynamicHS: streamlining Reiter’s hitting-set tree for sequential diagnosis. Information Sciences, 2023, 627: 251–279

[16] Shchekotykhin K, Schmitz T, Jannach D. Efficient sequential model-based fault-localization with partial diagnoses. In: Proceedings of the 25th International Joint Conference on Artificial Intelligence. 2016, 1251−1257

[17] Stern R, Juba B. Safe partial diagnosis from normal observations. In: Proceedings of the 33rd AAAI Conference on Artificial Intelligence. 2019, 3084−3091

[18] Cazes D, Kalech M. Model-based diagnosis with uncertain observations. In: Proceedings of the 34th AAAI Conference on Artificial Intelligence. 2020, 2766−2773

[19] Lamraoui S M, Nakajima S. A formula-based approach for automatic fault localization of imperative programs. In: Proceedings of the 16th International Conference on Formal Engineering Methods and Software Engineering. 2014, 251−266

[20] Lamraoui S M, Nakajima S . A formula-based approach for automatic fault localization of multi-fault programs. Journal of Information Processing, 2016, 24( 1): 88–98

[21] Ignatiev A, Morgado A, Weissenbacher G, Marques-Silva J. Model-based diagnosis with multiple observations. In: Proceeding of the 28th International Joint Conference on Artificial Intelligence. 2019, 1108−1115

[22] Zhou H, Ouyang D, Zhang L, Tian N . Model-based diagnosis with improved implicit hitting set dualization. Applied Intelligence, 2022, 52( 2): 2111–2118

[23] Zhou H, Ouyang D, Zhao X, Zhang L. Two compacted models for efficient model-based diagnosis. In: Proceedings of the 36th AAAI Conference on Artificial Intelligence. 2022, 3885−3893

[24] Kalech M, Stern R, Lazebnik E . Minimal cardinality diagnosis in problems with multiple observations. Diagnostics, 2021, 11( 5): 780

[25] Zhou H, Ouyang D, Tian X, Zhang L . DiagDO: an efficient model based diagnosis approach with multiple observations. Frontiers of Computer Science, 2023, 17( 6): 176407

[26] Tai R, Ouyang D, Liu W, Jiang L, Zhang L . A novel approach to model-based diagnosis with multiple observations. Engineering Applications of Artificial Intelligence, 2025, 141: 109768

[27] Jose M, Majumdar R . Cause clue clauses: error localization using maximum satisfiability. ACM SIGPLAN Notices, 2011, 46( 6): 437–446

[28] Lamraoui S M, Nakajima s. A formula-based approach for automatic fault localization of imperative programs. In: Proceedingd of the International Conference on Formal Engineering Methods. 2014, 251−266.

[29] Selman B, Kautz H A, Cohen B. Noise strategies for improving local search. In: Proceedings of the 12th National Conference on Artificial Intelligence. 1994, 337−343

[30] Balint A, Fröhlich A. Improving stochastic local search for sat with a new probability distribution. In: Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing. 2010, 10−15

[31] Cai S, Su K . Local search for Boolean satisfiability with configuration checking and subscore. Artificial Intelligence, 2013, 204: 75–98

[32] Fu H, Liu J, Wu G, Xu Y, Sutcliffe G . Improving probability selection based weights for satisfiability problems. Knowledge-Based Systems, 2022, 245: 108572

[33] Balint A, Biere A, Fröhlich A, Schöning U. Improving implementation of SLS solvers for SAT and new heuristics for k-SAT with long clauses. In: Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing–SAT 2014. 2014, 302−316

[34] Cha B, Iwama K, Kambayashi Y, Miyazaki S. Local search algorithms for partial MAXSAT. In: Proceedings of the 40th National Conference on Artificial Intelligence and 9th Conference on Innovative Applications of Artificial Intelligence. 1997, 263−268

[35] Luo C, Cai S, Wu W, Jie Z, Su K . CCLS: An efficient local search algorithm for weighted maximum satisfiability. IEEE Transactions on Computers, 2015, 64( 7): 1830–1843

[36] Thornton J, Sattar A. Dynamic constraint weighting for over-constrained problems. In: Proceedings of the 5th Pacific Rim International Conference on Artificial Intelligence. 1998, 377−388

[37] Thornton J, Bain S, Sattar A, Pham D N. A two level local search for MAX-SAT problems with hard and soft constraints. In: Proceedings of the 15th Australian Joint Conference on Artificial Intelligence. 2002, 603−614

[38] Cai S, Lei Z . Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability. Artificial Intelligence, 2020, 287: 103354

[39] Cai S, Luo C, Thornton J, Su K. Tailoring local search for partial MaxSAT. In: Proceedings of the 28th AAAI Conference on Artificial Intelligence. 2014, 2623−2629

[40] Luo C, Cai S, Su K, Huang W . CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability. Artificial Intelligence, 2017, 243: 26–44

[41] Chu Y, Cai S, Luo C. NUWLS: improving local search for (weighted) partial MaxSAT by new weighting techniques. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence. 2023, 3915−3923

[42] Chu Y, Li C M, Ye F, Cai S. Enhancing MaxSAT local search via a unified soft clause weighting scheme. In: Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing. 2024, 8

[43] Zheng J, He K, Zhou J. Farsighted probabilistic sampling: a general strategy for boosting local search MaxSAT solvers. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence. 2023, 4132−4139

[44] Zheng J, He K, Zhou J, Jin Y, Li C M, Manyà F . Integrating multi-armed bandit with local search for MaxSAT. Artificial Intelligence, 2025, 338: 104242

[45] Brglez F, Fujiwara H. A neutral netlist of 10 combinational benchmark circuits and a target translator in FORTRAN. In: Proceedings of the IEEE Symposium on Circuits and Systems. 1985, 663−698

[46] Corno F, Reorda M S, Squillero G . RT-level ITC’99 benchmarks and first ATPG results. IEEE Design & Test of Computers, 2000, 17( 3): 44–53

[47] Prikler L M, Wotawa F. Faster diagnosis with answer set programming (short paper). In: Proceedings of the 35th International Conference on Principles of Diagnosis and Resilient Systems (DX 2024). 2024, 24

[48] Zheng J, Chen Z, Li C M, He K. Rethinking the soft conflict pseudo Boolean constraint on MaxSAT local search solvers. In: Proceedings of the 33rd International Joint Conference on Artificial Intelligence. 2024, 1989−1997

RIGHTS & PERMISSIONS

Higher Education Press