{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T21:33:44Z","timestamp":1773351224004,"version":"3.50.1"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319232188","type":"print"},{"value":"9783319232195","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23219-5_13","type":"book-chapter","created":{"date-parts":[[2015,8,12]],"date-time":"2015-08-12T10:17:33Z","timestamp":1439374653000},"page":"173-182","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":29,"title":["Smallest MUS Extraction with Minimal Hitting Set Dualization"],"prefix":"10.1007","author":[{"given":"Alexey","family":"Ignatiev","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Previti","sequence":"additional","affiliation":[]},{"given":"Mark","family":"Liffiton","sequence":"additional","affiliation":[]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,13]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-39071-5_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"G Audemard","year":"2013","unstructured":"Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309\u2013317. Springer, Heidelberg (2013)"},{"issue":"2","key":"13_CR2","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":"13_CR3","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Chandrasekaran, K., Karp, R.M., Moreno-Centeno, E., Vempala, S.: Algorithms for implicit hitting set problems. In: SODA, pp. 614\u2013629 (2011)","DOI":"10.1137\/1.9781611973082.48"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-39071-5_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: A modular approach to MaxSAT modulo theories. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 150\u2013165. Springer, Heidelberg (2013)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-23786-7_19","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"J Davies","year":"2011","unstructured":"Davies, J., Bacchus, F.: Solving MAXSAT by solving a sequence of simpler SAT instances. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 225\u2013239. Springer, Heidelberg (2011)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-39071-5_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"J Davies","year":"2013","unstructured":"Davies, J., Bacchus, F.: Exploiting the power of mip solvers in maxsat. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 166\u2013181. Springer, Heidelberg (2013)"},{"key":"13_CR8","unstructured":"Gupta, A.: Learning Abstractions for Model Checking. PhD thesis, Carnegie Mellon University, June 2006"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-39071-5_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"A Ignatiev","year":"2013","unstructured":"Ignatiev, A., Janota, M., Marques-Silva, J.: Quantified maximum satisfiability: a core-guided approach. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 250\u2013266. Springer, Heidelberg (2013)"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Ignatiev, A., Janota, M., Marques-Silva, J.: Towards efficient optimization in package management systems. In: ICSE, pp. 745\u2013755 (2014)","DOI":"10.1145\/2568225.2568306"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-13509-5_14","volume-title":"Combinatorial Pattern Matching","author":"RM Karp","year":"2010","unstructured":"Karp, R.M.: Implicit hitting set problems and multi-genome alignment. In: Amir, A., Parida, L. (eds.) CPM 2010. LNCS, vol. 6129, pp. 151\u2013151. Springer, Heidelberg (2010)"},{"issue":"2","key":"13_CR12","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.artint.2004.11.002","volume":"163","author":"P Liberatore","year":"2005","unstructured":"Liberatore, P.: Redundancy in logic I: CNF propositional formulae. Artif. Intell. 163(2), 203\u2013232 (2005)","journal-title":"Artif. Intell."},{"issue":"4","key":"13_CR13","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/s10601-008-9058-8","volume":"14","author":"MH Liffiton","year":"2009","unstructured":"Liffiton, M.H., Mneimneh, M.N., Lynce, I., Andraus, Z.S., Marques-Silva, J., Sakallah, K.A.: A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints 14(4), 415\u2013442 (2009)","journal-title":"Constraints"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints (2015). http:\/\/dx.doi.org\/10.1007\/s10601-015-9183-0","DOI":"10.1007\/s10601-015-9183-0"},{"issue":"1","key":"13_CR15","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. Reasoning 40(1), 1\u201333 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Planes, J.: Algorithms for maximum satisfiability using unsatisfiable cores. In: DATE, pp. 408\u2013413 (2008)","DOI":"10.1145\/1403375.1403474"},{"issue":"1","key":"13_CR17","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. Intell. 32(1), 57\u201395 (1987)","journal-title":"Artif. Intell."},{"issue":"1","key":"13_CR18","first-page":"75","volume":"17","author":"C Sinz","year":"2003","unstructured":"Sinz, C., Kaiser, A., K\u00fcchlin, W.: Formal methods for the validation of automotive product configuration data. AI EDAM 17(1), 75\u201397 (2003)","journal-title":"AI EDAM"},{"key":"13_CR19","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, pp. 828\u2013834 (2012)","DOI":"10.1609\/aaai.v26i1.8231"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23219-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T08:01:49Z","timestamp":1676966509000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23219-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319232188","9783319232195"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23219-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"13 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}