{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T17:16:39Z","timestamp":1771262199424,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642215803","type":"print"},{"value":"9783642215810","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21581-0_14","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T13:30:19Z","timestamp":1307712619000},"page":"159-173","source":"Crossref","is-referenced-by-count":32,"title":["On Improving MUS Extraction Algorithms"],"prefix":"10.1007","author":[{"given":"Joao","family":"Marques-Silva","sequence":"first","affiliation":[]},{"given":"Ines","family":"Lynce","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Bakker, R.R., Dikker, F., Tempelman, F., Wognum, P.M.: Diagnosing and solving over-determined constraint satisfaction problems. In: International Joint Conference on Artificial Intelligence, pp. 276\u2013281 (1993)"},{"key":"14_CR2","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","volume":"2","author":"A. Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation\u00a02, 75\u201397 (2008)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"issue":"1","key":"14_CR3","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10472-005-0418-4","volume":"43","author":"R. Bruni","year":"2005","unstructured":"Bruni, R.: On exact selection of minimally unsatisfiable subformulae. Ann. Math. Artif. Intell.\u00a043(1), 35\u201350 (2005)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"2","key":"14_CR4","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","volume":"3","author":"J.W. Chinneck","year":"1991","unstructured":"Chinneck, J.W., Dravnieks, E.W.: Locating minimal infeasible constraint sets in linear programs. INFORMS Journal on Computing\u00a03(2), 157\u2013168 (1991)","journal-title":"INFORMS Journal on Computing"},{"key":"14_CR5","unstructured":"de Siqueira, J.L., Jean-Francois Puget, N.: Explanation-based generalisation of failures. In: European Conference on Artificial Intelligence, pp. 339\u2013344 (1988)"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11814948_5","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"N. Dershowitz","year":"2006","unstructured":"Dershowitz, N., Hanna, Z., Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 36\u201341. Springer, Heidelberg (2006)"},{"issue":"2","key":"14_CR7","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/s10878-008-9142-4","volume":"18","author":"C. Desrosiers","year":"2009","unstructured":"Desrosiers, C., Galinier, P., Hertz, A., Paroz, S.: Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems. J. Comb. Optim.\u00a018(2), 124\u2013150 (2009)","journal-title":"J. Comb. Optim."},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/S1574-6526(07)03002-7","volume-title":"Handbook of Knowledge Representation","author":"C.P. Gomes","year":"2008","unstructured":"Gomes, C.P., Kautz, H., Sabharwal, A., Selman, B.: Satisfiability solvers. In: Handbook of Knowledge Representation, pp. 89\u2013134. Elsevier, Amsterdam (2008)"},{"key":"14_CR9","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: Extracting MUSes. In: European Conference on Artificial Intelligence, pp. 387\u2013391 (August 2006)"},{"key":"14_CR10","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: Boosting a complete technique to find MSS and MUS thanks to a local search oracle. In: International Joint Conference on Artificial Intelligence, pp. 2300\u20132305 (January 2007)"},{"issue":"3","key":"14_CR11","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10601-007-9019-7","volume":"12","author":"\u00c9.. Gr\u00e9goire","year":"2007","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: Local-search extraction of MUSes. Constraints\u00a012(3), 325\u2013344 (2007)","journal-title":"Constraints"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: On approaches to explaining infeasibility of sets of Boolean clauses. In: International Conference on Tools with Artificial Intelligence, pp. 74\u201383 (November 2008)","DOI":"10.1109\/ICTAI.2008.39"},{"issue":"3","key":"14_CR13","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1016\/j.ejor.2007.06.066","volume":"199","author":"\u00c9. Gr\u00e9goire","year":"2009","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: Using local search to find MSSes and MUSes. European Journal of Operational Research\u00a0199(3), 640\u2013646 (2009)","journal-title":"European Journal of Operational Research"},{"key":"14_CR14","unstructured":"Hemery, F., Lecoutre, C., Sais, L., Boussemart, F.: Extracting MUCs from constraint networks. In: European Conference on Artificial Intelligence, pp. 113\u2013117 (2006)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Huang, J.: MUP: a minimal unsatisfiability prover. In: Asia South Pacific Design Automation, pp. 432\u2013437 (2005)","DOI":"10.1145\/1120725.1120907"},{"key":"14_CR16","unstructured":"Junker, U.: QUICKXPLAIN: Preferred explanations and relaxations for over-constrained problems. In: AAAI Conference on Artificial Intelligence, pp. 167\u2013172 (2004)"},{"issue":"2","key":"14_CR17","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/S0166-218X(02)00406-7","volume":"130","author":"O. Kullmann","year":"2003","unstructured":"Kullmann, O.: Lean clause-sets: generalizations of minimally unsatisfiable clause-sets. Discrete Applied Mathematics\u00a0130(2), 209\u2013249 (2003)","journal-title":"Discrete Applied Mathematics"},{"key":"14_CR18","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/SAT190075","volume":"7","author":"D. Le Berre","year":"2010","unstructured":"Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation\u00a07, 59\u201364 (2010)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"issue":"2","key":"14_CR19","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.\u00a0163(2), 203\u2013232 (2005)","journal-title":"Artif. Intell."},{"issue":"1","key":"14_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"M.H. Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning\u00a040(1), 1\u201333 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-79719-7_18","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"M.H. Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Searching for autarkies to trim unsatisfiable clause sets. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 182\u2013195. Springer, Heidelberg (2008)"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-642-02777-2_44","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M.H. Liffiton","year":"2009","unstructured":"Liffiton, M.H., Sakallah, K.A.: Generalizing core-guided max-SAT. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 481\u2013494. Springer, Heidelberg (2009)"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.: Minimal unsatisfiability: Models, algorithms and applications. In: International Symposium on Multiple-Valued Logic, pp. 9\u201314 (2010)","DOI":"10.1109\/ISMVL.2010.11"},{"key":"14_CR24","first-page":"131","volume-title":"SAT Handbook","author":"J. Marques-Silva","year":"2009","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) SAT Handbook, pp. 131\u2013154. IOS Press, Amsterdam (2009)"},{"key":"14_CR25","unstructured":"Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Formal Methods in Computer-Aided Design (October 2010)"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Oh, Y., Mneimneh, M.N., Andraus, Z.S., Sakallah, K.A., Markov, I.L.: AMUSE: a minimally-unsatisfiable subformula extractor. In: Design Automation Conference, pp. 518\u2013523 (2004)","DOI":"10.1145\/996566.996710"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-540-79719-7_27","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"H. Maaren van","year":"2008","unstructured":"van Maaren, H., Wieringa, S.: Finding guaranteed MUSes fast. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 291\u2013304. Springer, Heidelberg (2008)"},{"key":"14_CR28","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: Design, Automation and Test in Europe Conference, pp. 10880\u201310885 (2003)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2011"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21581-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,20]],"date-time":"2020-06-20T01:16:23Z","timestamp":1592615783000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21581-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642215803","9783642215810"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21581-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}