DVRE: dominator-based variables reduction of encoding for model-based diagnosis

Abstract

Compiling Model-Based Diagnosis to maximum satisfiability (MaxSAT) is currently a popular method because it can directly calculate the diagnosis. Although the method based on dominator component encoding can reduce the difficulty of the problem, with the increase of the system size, the complexity of the solution is also increasing. In this paper, we propose an efficient encoding method to solve this problem. The method makes several significant contributions. First, our strategy significantly reduces the size of the encoding required for constructing MaxSAT formulations in the offline phase, without the need for additional observations. Second, this strategy significantly decreases the number of clauses and variables through system observations, even when dealing with components that have uncertain output values. Last, our algorithm is applicable to both single and multiple observation diagnosis problems, without sacrificing the completeness of the solution set. Experimental results on ISCAS-85 benchmarks show that our algorithm outperforms the state-of-the-art algorithms on both single and multiple observation problems.

Graphical abstract

Keywords

model-based diagnosis / system observation / top-level diagnosis / cardinality-minimal diagnosis / satisfiability

References

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

[2] de Kleer J, Williams B C . Diagnosing multiple faults. Artificial Intelligence, 1987, 32( 1): 97–130

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

[4] Narasimhan S, Biswas G . Model-based diagnosis of hybrid systems. IEEE Transactions on Systems, Man, and Cybernetics – Part A: Systems and Humans, 2007, 37( 3): 348–361

[5] Safarpour S, Mangassarian H, Veneris A, Liffiton M H, Sakallah K A. Improved design debugging using maximum satisfiability. In: Proceedings of the Formal Methods in Computer Aided Design. 2007, 13−19

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

[7] Mordoch A, Juba B, Stern R. Learning safe numeric action models. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence. 2023, 12079−12086

[8] Christopher C J, Grastien A . Critical observations in model-based diagnosis. Artificial Intelligence, 2024, 331: 104116

[9] hiddiqi S A, Huang J B. Hierarchical diagnosis of multiple faults. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence. 2007, 581− 586

[10] Marques-Silva J, Janota M, Ignatiev A, Morgado A. Efficient model based diagnosis with maximum satisfiability. In: Proceedings of the 24th International Conference on Artificial Intelligence. 2015, 1966−1972

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

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

[13] Stern R, Kalech M, Feldman A, Provan G. Exploring the duality in conflict-directed model-based diagnosis. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence. 2012, 828−834

[14] Ansótegui C, Bonet M L, Levy J . SAT-based MaxSAT algorithms. Artificial Intelligence, 2013, 196: 77–105

[15] Feldman A B, Provan G, De Kleer J, Robert S, Van Gemund A J C. Solving model-based diagnosis problems with Max-SAT solvers and vice versa. In: Proceedings of the 21st International Workshop on the Principles of Diagnosis. 2010, 1−8

[16] Piotrów M. UWrMaxSat: efficient solver for MaxSAT and pseudo-Boolean problems. In: Proceedings of the 32nd International Conference on Tools with Artificial Intelligence. 2020, 132−136

[17] Williams B C, Ragno R J . Conflict-directed A* and its role in model-based embedded systems. Discrete Applied Mathematics, 2007, 155( 12): 1562–1595

[18] Feldman A, Provan G, Van Gemund A. Computing minimal diagnoses by greedy stochastic search. In: Proceedings of the 23rd National Conference on Artificial Intelligence. 2008, 911−918

[19] Jannach D, Schmitz T, Shchekotykhin K. Parallelized hitting set computation for model-based diagnosis. In: Proceedings of the 29th AAAI Conference on Artificial Intelligence. 2015, 1503−1510

[20] Metodi A, Stern R, Kalech M, Codish M . A novel SAT-based approach to model based diagnosis. Journal of Artificial Intelligence Research, 2014, 51: 377–411

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

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

[23] 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. 2014, 251−266

[24] 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

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

[26] Jiang L Y, Ouyang D T, Zhang Q, Zhang L M . DeciLS-PBO: an effective local search method for pseudo-Boolean optimization. Frontiers of Computer Science, 2024, 18( 2): 182326

[27] Luo C, Xing W Q, Cai S W, Hu C M . NuSC: an effective local search algorithm for solving the set covering problem. IEEE Transactions on Cybernetics, 2024, 54( 3): 1403–1416

[28] Cai S W, Li B H, Zhang X D . Local search for satisfiability modulo integer arithmetic theories. ACM Transactions on Computational Logic, 2023, 24( 4): 32

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

[30] Stern R, Kalech M, Rogov S, Feldman A. How many diagnoses do we need? Artificial Intelligence, 2017, 248: 26−45

[31] Bylander T, Allemang D, Tanner M C, Josephson J R. The computational complexity of abduction. Artificial Intelligence, 1991, 49(1−3): 25−60

[32] Köhl M A, Hermanns H . Model-based diagnosis of real-time systems: robustness against varying latency, clock drift, and out-of-order observations. ACM Transactions on Embedded Computing Systems, 2023, 22( 4): 68

[33] Rodler P . Sequential model-based diagnosis by systematic search. Artificial Intelligence, 2023, 323: 103988

[34] Elmishali A, Stern R, Kalech M. Data-augmented software diagnosis. In: Proceedings of the 30th AAAI Conference on Artificial Intelligence. 2016, 4003−4009

[35] Mencía C, Previti A, Marques-Silva J. Literal-based MCS extraction. In: Proceedings of the 24th International Conference on Artificial Intelligence. 2015, 1973−1979

RIGHTS & PERMISSIONS

Higher Education Press