{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T14:29:24Z","timestamp":1773930564720,"version":"3.50.1"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2024,12,16]],"date-time":"2024-12-16T00:00:00Z","timestamp":1734307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,12,16]],"date-time":"2024-12-16T00:00:00Z","timestamp":1734307200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2025,7]]},"DOI":"10.1007\/s11704-024-40894-w","type":"journal-article","created":{"date-parts":[[2024,12,16]],"date-time":"2024-12-16T06:28:17Z","timestamp":1734330497000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["DVRE: dominator-based variables reduction of encoding for model-based diagnosis"],"prefix":"10.1007","volume":"19","author":[{"given":"Jihong","family":"Ouyang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sen","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jinjin","family":"Chi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Liming","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,12,16]]},"reference":[{"issue":"1","key":"40894_CR1","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R Reiter","year":"1987","unstructured":"Reiter R. A theory of diagnosis from first principles. Artificial Intelligence, 1987, 32(1): 57\u201395","journal-title":"Artificial Intelligence"},{"issue":"1","key":"40894_CR2","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0004-3702(87)90063-4","volume":"32","author":"J de Kleer","year":"1987","unstructured":"de Kleer J, Williams B C. Diagnosing multiple faults. Artificial Intelligence, 1987, 32(1): 97\u2013130","journal-title":"Artificial Intelligence"},{"key":"40894_CR3","first-page":"326","volume-title":"Proceedings of the 15th International Symposium on Formal Methods","author":"E Torlak","year":"2008","unstructured":"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\u2013341"},{"issue":"3","key":"40894_CR4","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1109\/TSMCA.2007.893487","volume":"37","author":"S Narasimhan","year":"2007","unstructured":"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\u2013361","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics - Part A: Systems and Humans"},{"key":"40894_CR5","first-page":"13","volume-title":"Proceedings of the Formal Methods in Computer Aided Design","author":"S Safarpour","year":"2007","unstructured":"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\u201319"},{"issue":"6","key":"40894_CR6","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1145\/1993316.1993550","volume":"46","author":"M Jose","year":"2011","unstructured":"Jose M, Majumdar R. Cause clue clauses: error localization using maximum satisfiability. ACM SIGPLAN Notices, 2011, 46(6): 437\u2013446","journal-title":"ACM SIGPLAN Notices"},{"key":"40894_CR7","first-page":"12079","volume-title":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","author":"A Mordoch","year":"2023","unstructured":"Mordoch A, Juba B, Stern R. Learning safe numeric action models. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence. 2023, 12079\u201312086"},{"key":"40894_CR8","doi-asserted-by":"publisher","first-page":"104116","DOI":"10.1016\/j.artint.2024.104116","volume":"331","author":"C J Christopher","year":"2024","unstructured":"Christopher C J, Grastien A. Critical observations in model-based diagnosis. Artificial Intelligence, 2024, 331: 104116","journal-title":"Artificial Intelligence"},{"key":"40894_CR9","first-page":"581","volume-title":"Proceedings of the 20th International Joint Conference on Artificial Intelligence","author":"S A Hiddiqi","year":"2007","unstructured":"Hiddiqi S A, Huang J B. Hierarchical diagnosis of multiple faults. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence. 2007, 581\u2013586"},{"key":"40894_CR10","first-page":"1966","volume-title":"Proceedings of the 24th International Conference on Artificial Intelligence","author":"J Marques-Silva","year":"2015","unstructured":"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\u20131972"},{"key":"40894_CR11","first-page":"1108","volume-title":"Proceedings of the 28th International Conference on Artificial Intelligence","author":"A Ignatiev","year":"2019","unstructured":"Ignatiev A, Morgado A, Weissenbacher G, Marques-Silva J. Modelbased diagnosis with multiple observations. In: Proceedings of the 28th International Conference on Artificial Intelligence. 2019, 1108\u20131115"},{"key":"40894_CR12","doi-asserted-by":"publisher","first-page":"103354","DOI":"10.1016\/j.artint.2020.103354","volume":"287","author":"S W Cai","year":"2020","unstructured":"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","journal-title":"Artificial Intelligence"},{"key":"40894_CR13","first-page":"828","volume-title":"Proceedings of the 26th AAAI Conference on Artificial Intelligence","author":"R Stern","year":"2012","unstructured":"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\u2013834"},{"key":"40894_CR14","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.artint.2013.01.002","volume":"196","author":"C Ans\u00f3tegui","year":"2013","unstructured":"Ans\u00f3tegui C, Bonet M L, Levy J. SAT-based MaxSAT algorithms. Artificial Intelligence, 2013, 196: 77\u2013105","journal-title":"Artificial Intelligence"},{"key":"40894_CR15","first-page":"1","volume-title":"Proceedings of the 21st International Workshop on the Principles of Diagnosis","author":"A B Feldman","year":"2010","unstructured":"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\u20138"},{"key":"40894_CR16","first-page":"132","volume-title":"Proceedings of the 32nd International Conference on Tools with Artificial Intelligence","author":"M Piotr\u00f3w","year":"2020","unstructured":"Piotr\u00f3w M. UWrMaxSat: efficient solver for MaxSAT and pseudo-Boolean problems. In: Proceedings of the 32nd International Conference on Tools with Artificial Intelligence. 2020, 132\u2013136"},{"issue":"12","key":"40894_CR17","doi-asserted-by":"publisher","first-page":"1562","DOI":"10.1016\/j.dam.2005.10.022","volume":"155","author":"B C Williams","year":"2007","unstructured":"Williams B C, Ragno R J. Conflict-directed A* and its role in modelbased embedded systems. Discrete Applied Mathematics, 2007, 155(12): 1562\u20131595","journal-title":"Discrete Applied Mathematics"},{"key":"40894_CR18","first-page":"911","volume-title":"Proceedings of the 23rd National Conference on Artificial Intelligence","author":"A Feldman","year":"2008","unstructured":"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\u2013918"},{"key":"40894_CR19","first-page":"1503","volume-title":"Proceedings of the 29th AAAI Conference on Artificial Intelligence","author":"D Jannach","year":"2015","unstructured":"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\u20131510"},{"key":"40894_CR20","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1613\/jair.4503","volume":"51","author":"A Metodi","year":"2014","unstructured":"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\u2013411","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"2","key":"40894_CR21","doi-asserted-by":"publisher","first-page":"2111","DOI":"10.1007\/s10489-021-02408-0","volume":"52","author":"H S Zhou","year":"2022","unstructured":"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\u20132118","journal-title":"Applied Intelligence"},{"key":"40894_CR22","first-page":"3885","volume-title":"Proceedings of the 36th AAAI Conference on Artificial Intelligence","author":"H S Zhou","year":"2022","unstructured":"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\u20133893"},{"key":"40894_CR23","first-page":"251","volume-title":"Proceedings of the 16th International Conference on Formal Engineering Methods","author":"S M Lamraoui","year":"2014","unstructured":"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\u2013266"},{"issue":"1","key":"40894_CR24","doi-asserted-by":"publisher","first-page":"88","DOI":"10.2197\/ipsjjip.24.88","volume":"24","author":"S M Lamraoui","year":"2016","unstructured":"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\u201398","journal-title":"Journal of Information Processing"},{"issue":"6","key":"40894_CR25","doi-asserted-by":"publisher","first-page":"176407","DOI":"10.1007\/s11704-022-2261-8","volume":"17","author":"H S Zhou","year":"2023","unstructured":"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","journal-title":"Frontiers of Computer Science"},{"issue":"2","key":"40894_CR26","doi-asserted-by":"publisher","first-page":"182326","DOI":"10.1007\/s11704-023-3018-8","volume":"18","author":"L Y Jiang","year":"2024","unstructured":"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","journal-title":"Frontiers of Computer Science"},{"issue":"3","key":"40894_CR27","doi-asserted-by":"publisher","first-page":"1403","DOI":"10.1109\/TCYB.2022.3199147","volume":"54","author":"C Luo","year":"2024","unstructured":"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\u20131416","journal-title":"IEEE Transactions on Cybernetics"},{"issue":"4","key":"40894_CR28","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/3597495","volume":"24","author":"S W Cai","year":"2023","unstructured":"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","journal-title":"ACM Transactions on Computational Logic"},{"issue":"5","key":"40894_CR29","doi-asserted-by":"publisher","first-page":"780","DOI":"10.3390\/diagnostics11050780","volume":"11","author":"M Kalech","year":"2021","unstructured":"Kalech M, Stern R, Lazebnik E. Minimal cardinality diagnosis in problems with multiple observations. Diagnostics, 2021, 11(5): 780","journal-title":"Diagnostics"},{"key":"40894_CR30","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.artint.2017.03.002","volume":"248","author":"R Stern","year":"2017","unstructured":"Stern R, Kalech M, Rogov S, Feldman A. How many diagnoses do we need? Artificial Intelligence, 2017, 248: 26\u201345","journal-title":"Artificial Intelligence"},{"issue":"1\u20133","key":"40894_CR31","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0004-3702(91)90005-5","volume":"49","author":"T Bylander","year":"1991","unstructured":"Bylander T, Allemang D, Tanner M C, Josephson J R. The computational complexity of abduction. Artificial Intelligence, 1991, 49(1\u20133): 25\u201360","journal-title":"Artificial Intelligence"},{"issue":"4","key":"40894_CR32","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/3597209","volume":"22","author":"M A K\u00f6hl","year":"2023","unstructured":"K\u00f6hl 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","journal-title":"ACM Transactions on Embedded Computing Systems"},{"key":"40894_CR33","doi-asserted-by":"publisher","first-page":"103988","DOI":"10.1016\/j.artint.2023.103988","volume":"323","author":"P Rodler","year":"2023","unstructured":"Rodler P. Sequential model-based diagnosis by systematic search. Artificial Intelligence, 2023, 323: 103988","journal-title":"Artificial Intelligence"},{"key":"40894_CR34","first-page":"4003","volume-title":"Proceedings of the 30th AAAI Conference on Artificial Intelligence","author":"A Elmishali","year":"2016","unstructured":"Elmishali A, Stern R, Kalech M. Data-augmented software diagnosis. In: Proceedings of the 30th AAAI Conference on Artificial Intelligence. 2016, 4003\u20134009"},{"key":"40894_CR35","first-page":"1973","volume-title":"Proceedings of the 24th International Conference on Artificial Intelligence","author":"C Menc\u00eda","year":"2015","unstructured":"Menc\u00eda C, Previti A, Marques-Silva J. Literal-based MCS extraction. In: Proceedings of the 24th International Conference on Artificial Intelligence. 2015, 1973\u20131979"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-024-40894-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11704-024-40894-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-024-40894-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,16]],"date-time":"2024-12-16T07:16:04Z","timestamp":1734333364000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11704-024-40894-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,16]]},"references-count":35,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2025,7]]}},"alternative-id":["40894"],"URL":"https:\/\/doi.org\/10.1007\/s11704-024-40894-w","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12,16]]},"assertion":[{"value":"24 August 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 October 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 December 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"<b>Competing interests<\/b> The authors declare that they have no competing interests or financial conflicts to disclose.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethics"}}],"article-number":"197349"}}