{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T14:29:22Z","timestamp":1773930562250,"version":"3.50.1"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"11","license":[{"start":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T00:00:00Z","timestamp":1526601600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2018,11]]},"DOI":"10.1007\/s11432-017-9273-5","type":"journal-article","created":{"date-parts":[[2018,5,28]],"date-time":"2018-05-28T03:07:12Z","timestamp":1527476832000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Efficient zonal diagnosis with maximum satisfiability"],"prefix":"10.1007","volume":"61","author":[{"given":"Meng","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dantong","family":"Ouyang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaowei","family":"Cai","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":[[2018,5,18]]},"reference":[{"key":"9273_CR1","first-page":"1393","volume-title":"Proceedings of the 16th International Joint Conference on Artificial Intelligence, Stockholm","author":"L Console","year":"1999","unstructured":"Console L, Dressler O. Model-based diagnosis in the real world: lessons learned and challenges remaining. In: Proceedings of the 16th International Joint Conference on Artificial Intelligence, Stockholm, 1999. 1393\u20131400"},{"key":"9273_CR2","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/j.tcs.2006.01.001","volume":"355","author":"K Xu","year":"2006","unstructured":"Xu K, Li W. Many hard examples in exact phase transitions. Theory Comput Sci, 2006, 355: 291\u2013302","journal-title":"Theory Comput Sci"},{"key":"9273_CR3","doi-asserted-by":"publisher","first-page":"062103","DOI":"10.1007\/s11432-015-5377-8","volume":"60","author":"Y Y Wang","year":"2017","unstructured":"Wang Y Y, Ouyang D T, Zhang L M, et al. A novel local search for unicost set covering problem using hyperedge configuration checking and weight diversity. Sci China Inf Sci, 2017, 60: 062103","journal-title":"Sci China Inf Sci"},{"key":"9273_CR4","first-page":"032104","volume":"58","author":"J Gao","year":"2015","unstructured":"Gao J, Wang J N, Yin M H. Experimental analyses on phase transitions in compiling satisfiability problems. Sci China Inf Sci, 2015, 58: 032104","journal-title":"Sci China Inf Sci"},{"key":"9273_CR5","doi-asserted-by":"publisher","first-page":"012205","DOI":"10.1007\/s11432-015-0897-0","volume":"60","author":"X N Geng","year":"2017","unstructured":"Geng X N, Ouyang D T, Zhang Y G. Model-based diagnosis of incomplete discrete-event system with rough set theory. Sci China Inf Sci, 2017, 60: 012205","journal-title":"Sci China Inf Sci"},{"key":"9273_CR6","doi-asserted-by":"publisher","first-page":"092112","DOI":"10.1007\/s11432-016-9057-8","volume":"60","author":"X Y Wang","year":"2017","unstructured":"Wang X Y, Jiang S J, Gao P F, et al. Cost-effective testing based fault localization with distance based test-suite reduction. Sci China Inf Sci, 2017, 60: 092112","journal-title":"Sci China Inf Sci"},{"key":"9273_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1142\/S0129054112500025","volume":"23","author":"J P Zhou","year":"2012","unstructured":"Zhou J P, Yin M H, Li X T, et al. Phase transitions of expspace-complete problems: a further step. Int J Found Comput Sci, 2012, 23: 173\u2013184","journal-title":"Int J Found Comput Sci"},{"key":"9273_CR8","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/0004-3702(92)90027-U","volume":"56","author":"J Kleer de","year":"1992","unstructured":"de Kleer J, Mackworth A K, Reiter R. Characterizing diagnoses and systems. Artif Intel, 1992, 56: 197\u2013222","journal-title":"Artif Intel"},{"key":"9273_CR9","volume-title":"US Patent","author":"K J De","year":"2017","unstructured":"De K J. US Patent, 9563525, 2017\u201302-07"},{"key":"9273_CR10","first-page":"1503","volume-title":"Proceedings of the 29th^AAAI Conference on Artificial Intelligence, Austin","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, Austin, 2015. 1503\u20131510"},{"key":"9273_CR11","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 model-based embedded systems. Discrete Appl Math, 2007, 155: 1562\u20131595","journal-title":"Discrete Appl Math"},{"key":"9273_CR12","first-page":"185","volume-title":"Proceedings of the 21th International Workshop on Principles of Diagnosis, Portland","author":"A Feldman","year":"2010","unstructured":"Feldman A, Provan G, de Kleer J, et al. Solving model-based diagnosis problems with max-sat solvers and vice versa. In: Proceedings of the 21th International Workshop on Principles of Diagnosis, Portland, 2010. 185\u2013192"},{"key":"9273_CR13","first-page":"793","volume-title":"Proceedings of the 26th^AAAI Conference on Artificial Intelligence, Toronto","author":"A Metodi","year":"2012","unstructured":"Metodi A, Stern R, Kalech M, et al. Compiling model-based diagnosis to boolean satisfaction. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence, Toronto, 2012. 793\u2013799"},{"key":"9273_CR14","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, et al. A novel sat-based approach to model based diagnosis. J Artif Intell Res, 2014, 51: 377\u2013411","journal-title":"J Artif Intell Res"},{"key":"9273_CR15","first-page":"186","volume-title":"Proceedings of the 15th Theory and Applications of Satisfiability Testing, Trento","author":"J Zhang","year":"2012","unstructured":"Zhang J, Ma F F, Zhang Z Q. Faulty interaction identification via constraint solving and optimization. In: Proceedings of the 15th Theory and Applications of Satisfiability Testing, Trento, 2012. 186\u2013199"},{"key":"9273_CR16","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1145\/502090.502091","volume":"48","author":"A Darwiche","year":"2001","unstructured":"Darwiche A. Decomposable negation normal form. J ACM, 2001, 48: 608\u2013647","journal-title":"J ACM"},{"key":"9273_CR17","first-page":"581","volume-title":"Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad","author":"S Siddiqi","year":"2007","unstructured":"Siddiqi S, Huang J B. Hierarchical diagnosis of multiple faults. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, 2007. 581\u2013586"},{"key":"9273_CR18","first-page":"828","volume-title":"Proceedings of the 26th^AAAI Conference on Artificial Intelligence, Toronto","author":"R Stern","year":"2012","unstructured":"Stern R, Kalech M, Feldman A, et al. Exploring the duality in conflict-directed model-based diagnosis. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence, Toronto, 2012. 828\u2013834"},{"key":"9273_CR19","doi-asserted-by":"publisher","first-page":"1606","DOI":"10.1109\/TCAD.2005.852031","volume":"24","author":"A Smith","year":"2005","unstructured":"Smith A, Veneris A, Ali M F, et al. Fault diagnosis and logic debugging using Boolean satisfiability. IEEE Trans Comput-Aided Design, 2005, 24: 1606\u20131621","journal-title":"IEEE Trans Comput-Aided Design"},{"key":"9273_CR20","first-page":"240","volume-title":"Proceedings of the 26th International Conference on Computer-Aided Design, San Jose","author":"H Mangassarian","year":"2007","unstructured":"Mangassarian H, Veneris A, Safarpour S, et al. A performance-driven QBF-based iterative logic array representation with applications to verification, debug and test. In: Proceedings of the 26th International Conference on Computer-Aided Design, San Jose, 2007. 240\u2013245"},{"key":"9273_CR21","first-page":"77","volume-title":"Proceedings of the 18th^ACM Great Lakes Symposium on VLSI, Orlando","author":"A Suelflow","year":"2008","unstructured":"Suelflow A, Fey G, Bloem R, et al. Using unsatisfiable cores to debug multiple design errors. In: Proceedings of the 18th ACM Great Lakes Symposium on VLSI, Orlando, 2008. 77\u201382"},{"key":"9273_CR22","first-page":"1182","volume-title":"Proceedings of the 10th Design","author":"S Safarpour","year":"2007","unstructured":"Safarpour S, Veneris A. Abstraction and refinement techniques in automated design debugging. In: Proceedings of the 10th Design, Automation and Test in Europe Conference and Exhibition, Nice, 2007. 1182\u20131187"},{"key":"9273_CR23","doi-asserted-by":"publisher","first-page":"092109","DOI":"10.1007\/s11432-016-0258-4","volume":"60","author":"J Gao","year":"2017","unstructured":"Gao J, Li R Z, Yin M H. A randomized diversification strategy for solving satisfiability problem with long clauses. Sci China Inf Sci, 2017, 60: 092109","journal-title":"Sci China Inf Sci"},{"key":"9273_CR24","doi-asserted-by":"publisher","first-page":"092101","DOI":"10.1007\/s11432-016-5526-8","volume":"59","author":"J Liu","year":"2016","unstructured":"Liu J, Xu K. A novel weighting scheme for random k-SAT. Sci China Inf Sci, 2016, 59: 092101","journal-title":"Sci China Inf Sci"},{"key":"9273_CR25","first-page":"13","volume-title":"Proceedings of the 7th Formal Methods in Computer Aided Design, Austin","author":"S Safarpour","year":"2007","unstructured":"Safarpour S, Mangassarian H, Veneris A, et al. Improved design debugging using maximum satisfiability. In: Proceedings of the 7th Formal Methods in Computer Aided Design, Austin, 2007. 13\u201319"},{"key":"9273_CR26","first-page":"99","volume-title":"Proceedings of the 20th International Workshop on Principles of Diagnosis, Stockholm","author":"T Kutsuna","year":"2009","unstructured":"Kutsuna T, Sato S, Chujo N. Diagnosing automotive control systems using abstract model-based diagnosis. In: Proceedings of the 20th International Workshop on Principles of Diagnosis, Stockholm, 2009. 99\u2013105"},{"key":"9273_CR27","first-page":"345","volume-title":"Proceedings of the 19th^ACM Great Lakes Symposium on VLSI, Boston Area","author":"Y B Chen","year":"2009","unstructured":"Chen Y B, Safarpour S, Veneris A, et al. Spatial and temporal design debug using partial MaxSAT. In: Proceedings of the 19th ACM Great Lakes Symposium on VLSI, Boston Area, 2009. 345\u2013350"},{"key":"9273_CR28","first-page":"2623","volume-title":"Proceedings of the 28th AAAI Conference on Artificial Intelligence, Quebec","author":"S W Cai","year":"2014","unstructured":"Cai S W, Luo C, Thornton J, et al. Tailoring local search for partial MaxSAT. In: Proceedings of the 28th AAAI Conference on Artificial Intelligence, Quebec, 2014. 2623\u20132629"},{"key":"9273_CR29","first-page":"1966","volume-title":"Proceedings of the 24th International Joint Conference on Artificial Intelligence, Buenos Aires","author":"J Marques-Silva","year":"2015","unstructured":"Marques-Silva J, Janota M, Ignatiev A, et al. Efficient model based diagnosis with maximum satisfiability. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence, Buenos Aires, 2015. 1966\u20131972"},{"key":"9273_CR30","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1145\/37888.37963","volume-title":"Proceedings of the 24th ACM\/IEEE Design Automation Conference, Miami Beach","author":"T Kirkland","year":"1987","unstructured":"Kirkland T, Mercer M. A topological search algorithm for ATPG. In: Proceedings of the 24th ACM\/IEEE Design Automation Conference, Miami Beach, 1987. 502\u2013508"},{"key":"9273_CR31","first-page":"300","volume-title":"Proceedings of the 20th National Conference on Artificial Intelligence, London","author":"J B Huang","year":"2005","unstructured":"Huang J B, Darwiche A. On compiling system models for faster and more scalable diagnosis. In: Proceedings of the 20th National Conference on Artificial Intelligence, London, 2005. 300\u2013306"},{"key":"9273_CR32","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. Artif Intel, 1987, 32: 57\u201395","journal-title":"Artif Intel"},{"key":"9273_CR33","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0004-3702(87)90063-4","volume":"32","author":"J Kleer de","year":"1987","unstructured":"de Kleer J, Williams B C. Diagnosing multiple faults. Artif Intel, 1987, 32: 97\u2013130","journal-title":"Artif Intel"},{"key":"9273_CR34","first-page":"1087","volume-title":"Proceedings of the 20th International Joint Conference on Artificial Intelligence, Barcelona","author":"S Siddiqi","year":"2011","unstructured":"Siddiqi S. Computing minimum-cardinality diagnoses by model relaxation. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, Barcelona, 2011. 1087\u20131092"},{"key":"9273_CR35","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-319-10428-7_39","volume-title":"Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming, Lyon","author":"R Martins","year":"2014","unstructured":"Martins R, Joshi S, Manquinho V, et al. Incremental cardinality constraints for MaxSAT. In: Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming, Lyon, 2014. 531\u2013548"},{"key":"9273_CR36","first-page":"1039","volume-title":"Proceedings of the 22th International Joint Conference on Artificial Intelligence, Beijing","author":"I Nica","year":"2013","unstructured":"Nica I, Pill I, Quaritsch T, et al. The route to success-a performance comparison of diagnosis algorithms. In: Proceedings of the 22th International Joint Conference on Artificial Intelligence, Beijing, 2013. 1039\u20131045"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-017-9273-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-017-9273-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-017-9273-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,19]],"date-time":"2019-12-19T10:24:22Z","timestamp":1576751062000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-017-9273-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,18]]},"references-count":36,"journal-issue":{"issue":"11","published-print":{"date-parts":[[2018,11]]}},"alternative-id":["9273"],"URL":"https:\/\/doi.org\/10.1007\/s11432-017-9273-5","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"value":"1674-733X","type":"print"},{"value":"1869-1919","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,5,18]]},"assertion":[{"value":"11 July 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 August 2017","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 September 2017","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 May 2018","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"112101"}}