{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T17:14:30Z","timestamp":1725988470374},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319999562"},{"type":"electronic","value":"9783319999579"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99957-9_7","type":"book-chapter","created":{"date-parts":[[2018,8,21]],"date-time":"2018-08-21T04:26:31Z","timestamp":1534825591000},"page":"104-118","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets"],"prefix":"10.1007","author":[{"given":"Shaofan","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie","family":"Luo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,22]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-33954-2_3","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"F Bacchus","year":"2016","unstructured":"Bacchus, F., Katsirelos, G.: Finding a collection of MUSes incrementally. In: Quimper, C.-G. (ed.) CPAIOR 2016. LNCS, vol. 9676, pp. 35\u201344. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33954-2_3"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-30557-6_14","volume-title":"Practical Aspects of Declarative Languages","author":"J Bailey","year":"2005","unstructured":"Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2005. LNCS, vol. 3350, pp. 174\u2013186. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30557-6_14"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"de la Banda, M.G., Stuckey, P.J., Wazny, J.: Finding all minimal unsatisfiable subsets. In: Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming, pp. 32\u201343. ACM (2003)","DOI":"10.1145\/888251.888256"},{"issue":"2","key":"7_CR4","doi-asserted-by":"crossref","first-page":"97","DOI":"10.3233\/AIC-2012-0523","volume":"25","author":"A Belov","year":"2012","unstructured":"Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97\u2013116 (2012)","journal-title":"AI Commun."},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"7_CR7","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/S1574-6526(07)03002-7","volume":"3","author":"CP Gomes","year":"2008","unstructured":"Gomes, C.P., Kautz, H., Sabharwal, A., Selman, B.: Satisfiability solvers. Found. Artifi. Intell. 3, 89\u2013134 (2008)","journal-title":"Found. Artifi. Intell."},{"issue":"2","key":"7_CR8","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/0004-3702(94)90019-1","volume":"65","author":"A Hou","year":"1994","unstructured":"Hou, A.: A theory of measurement in diagnosis from first principles. Artif. Intell. 65(2), 281\u2013328 (1994)","journal-title":"Artif. Intell."},{"issue":"1\u20132","key":"7_CR9","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/s10472-010-9191-0","volume":"60","author":"F Hutter","year":"2010","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K.: Tradeoffs in the empirical evaluation of competing algorithm designs. Ann. Math. Artif. Intell. 60(1\u20132), 65\u201389 (2010)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"01n02","key":"7_CR10","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1142\/S0218213095000103","volume":"4","author":"W Li","year":"1995","unstructured":"Li, W., Shen, N., Wang, J.: R-calculus: a logical approach for knowledge base maintenance. Int. J. Artif. Intell. Tools 4(01n02), 177\u2013200 (1995)","journal-title":"Int. J. Artif. Intell. Tools"},{"issue":"2","key":"7_CR11","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10601-015-9183-0","volume":"21","author":"MH Liffiton","year":"2016","unstructured":"Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints 21(2), 223\u2013250 (2016)","journal-title":"Constraints"},{"issue":"1","key":"7_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1\u201333 (2008)","journal-title":"J. Autom. Reason."},{"issue":"12","key":"7_CR13","doi-asserted-by":"publisher","first-page":"2530","DOI":"10.1007\/s11432-011-4492-4","volume":"54","author":"J Luo","year":"2011","unstructured":"Luo, J., Li, W.: R-calculus without the cut rule. Sci. China Inf. Sci. 54(12), 2530\u20132543 (2011)","journal-title":"Sci. China Inf. Sci."},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Previti, A., Marques-Silva, J.: Partial MUS enumeration. In: AAAI (2013)","DOI":"10.1609\/aaai.v27i1.8657"},{"key":"7_CR15","series-title":"Modern Birkh\u00e4user Classics","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-0-8176-4842-8_1","volume-title":"Classic Papers in Combinatorics","author":"FP Ramsey","year":"2009","unstructured":"Ramsey, F.P.: On a problem of formal logic. In: Gessel, I., Rota, G.C. (eds.) Classic Papers in Combinatorics. MBC, pp. 1\u201324. Springer, Boston (2009). https:\/\/doi.org\/10.1007\/978-0-8176-4842-8_1"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-21581-0_15","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"V Ryvchin","year":"2011","unstructured":"Ryvchin, V., Strichman, O.: Faster extraction of high-level minimal unsatisfiable cores. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 174\u2013187. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21581-0_15"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Stern, R.T., Kalech, M., Feldman, A., Provan, G.M.: Exploring the duality in conflict-directed model-based diagnosis. In: AAAI, vol. 12, pp. 828\u2013834 (2012)","DOI":"10.1609\/aaai.v26i1.8231"},{"issue":"4","key":"7_CR18","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 59(4), 483\u2013502 (2017)","journal-title":"J. Autom. Reason."},{"key":"7_CR19","unstructured":"Xiao, G., Ma, Y.: Inconsistency measurement based on variables in minimal unsatisfiable subsets. In: European Conference on Artificial Intelligence 2012 (ECAI 2012) (2012)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Xie, H., Luo, J.: An algorithm to compute minimal unsatisfiable subsets for a decidable fragment of first-order formulas. In: 2016 IEEE 28th International Conference on Tools with Artificial Intelligence (ICTAI), pp. 444\u2013451. IEEE (2016)","DOI":"10.1109\/ICTAI.2016.0074"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99957-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T18:08:50Z","timestamp":1661796530000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99957-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319999562","9783319999579"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99957-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}