{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,14]],"date-time":"2025-11-14T21:28:36Z","timestamp":1763155716069},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397981"},{"type":"electronic","value":"9783642397998"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_39","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T19:13:06Z","timestamp":1373483586000},"page":"592-607","source":"Crossref","is-referenced-by-count":35,"title":["Minimal Sets over Monotone Predicates in Boolean Formulae"],"prefix":"10.1007","author":[{"given":"Joao","family":"Marques-Silva","sequence":"first","affiliation":[]},{"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"additional","affiliation":[]},{"given":"Anton","family":"Belov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"39_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-540-89439-1_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Z.S. Andraus","year":"2008","unstructured":"Andraus, Z.S., Liffiton, M.H., Sakallah, K.A.: Reveal: A formal verification tool for verilog designs. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 343\u2013352. Springer, Heidelberg (2008)"},{"key":"39_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 2004. LNCS, vol.\u00a03350, pp. 174\u2013186. Springer, Heidelberg (2005)"},{"key":"39_CR3","unstructured":"Bakker, R.R., Dikker, F., Tempelman, F., Wognum, P.M.: Diagnosing and solving over-determined constraint satisfaction problems. In: IJCAI, pp. 276\u2013281 (1993)"},{"key":"39_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-33558-7_14","volume-title":"Principles and Practice of Constraint Programming","author":"A. Belov","year":"2012","unstructured":"Belov, A., Janota, M., Lynce, I., Marques-Silva, J.: On computing minimal equivalent subformulas. In: Milano, M. (ed.) CP 2012. LNCS, vol.\u00a07514, pp. 158\u2013174. Springer, Heidelberg (2012)"},{"issue":"2","key":"39_CR5","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.\u00a025(2), 97\u2013116 (2012)","journal-title":"AI Commun."},{"key":"39_CR6","first-page":"123","volume":"8","author":"A. Belov","year":"2012","unstructured":"Belov, A., Marques-Silva, J.: MUSer2: An efficient MUS extractor, system description. JSAT\u00a08, 123\u2013128 (2012)","journal-title":"JSAT"},{"key":"39_CR7","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press (2009)"},{"key":"39_CR8","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: FMCAD, pp. 173\u2013180 (2007)","DOI":"10.1109\/FAMCAD.2007.15"},{"issue":"4-5","key":"39_CR9","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s00165-008-0080-9","volume":"20","author":"A.R. Bradley","year":"2008","unstructured":"Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Asp. Comput.\u00a020(4-5), 379\u2013405 (2008)","journal-title":"Formal Asp. Comput."},{"issue":"3-4","key":"39_CR10","first-page":"137","volume":"10","author":"M. Cadoli","year":"1997","unstructured":"Cadoli, M., Donini, F.M.: A survey on knowledge compilation. AI Commun.\u00a010(3-4), 137\u2013150 (1997)","journal-title":"AI Commun."},{"issue":"2","key":"39_CR11","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":"39_CR12","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A. Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. (JAIR)\u00a017, 229\u2013264 (2002)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"39_CR13","unstructured":"de Siqueira, J.L.,, N., Puget, J.-F.: Explanation-based generalisation of failures. In: ECAI, pp. 339\u2013344 (1988)"},{"key":"39_CR14","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":"1","key":"39_CR15","first-page":"53","volume":"26","author":"A. Felfernig","year":"2012","unstructured":"Felfernig, A., Schubert, M., Zehentner, C.: An efficient diagnosis algorithm for inconsistent constraint sets. AI EDAM\u00a026(1), 53\u201362 (2012)","journal-title":"AI EDAM"},{"key":"39_CR16","doi-asserted-by":"crossref","unstructured":"Gomes, C.P., Kautz, H., Sabharwal, A., Selman, B.: Satisfiability solvers. In: Frank van Harmelen, V.L., Porter, B. (eds.) Handbook of Knowledge Representation, vol.\u00a03, pp. 89\u2013134 (2008)","DOI":"10.1016\/S1574-6526(07)03002-7"},{"key":"39_CR17","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: On approaches to explaining infeasibility of sets of Boolean clauses. In: ICTAI, pp. 74\u201383 (November 2008)","DOI":"10.1109\/ICTAI.2008.39"},{"key":"39_CR18","unstructured":"Hemery, F., Lecoutre, C., Sais, L., Boussemart, F.: Extracting MUCs from constraint networks. In: ECAI, pp. 113\u2013117 (2006)"},{"key":"39_CR19","unstructured":"Junker, U.: QUICKXPLAIN: Preferred explanations and relaxations for over-constrained problems. In: AAAI, pp. 167\u2013172 (2004)"},{"key":"39_CR20","unstructured":"Kottler, S.: Description of the SApperloT, SArTagnan and MoUsSaka solvers for the SAT-Competition 2011 (2011), http:\/\/www.satcompetition.org\/2011\/"},{"issue":"1","key":"39_CR21","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":"39_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-642-21581-0_14","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"J. Marques-Silva","year":"2011","unstructured":"Marques-Silva, J., Lynce, I.: On improving MUS extraction algorithms. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 159\u2013173. Springer, Heidelberg (2011)"},{"key":"39_CR23","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.) Handbook of Satisfiability, pp. 131\u2013153. IOS Press (2009)"},{"key":"39_CR24","doi-asserted-by":"crossref","unstructured":"Marquis, P.: Consequence finding algorithms. In: Algorithms for Defeasible and Uncertain Reasoning. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-94-017-1737-3_3"},{"issue":"1-2","key":"39_CR25","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0004-3702(80)90011-9","volume":"13","author":"J. McCarthy","year":"1980","unstructured":"McCarthy, J.: Circumscription - a form of non-monotonic reasoning. Artif. Intell.\u00a013(1-2), 27\u201339 (1980)","journal-title":"Artif. Intell."},{"key":"39_CR26","unstructured":"Nadel, A.: Boosting minimal unsatisfiable core extraction. In: FMCAD, pp. 121\u2013128 (October 2010)"},{"key":"39_CR27","doi-asserted-by":"crossref","unstructured":"N\u00f6hrer, A., Biere, A., Egyed, A.: Managing SAT inconsistencies with HUMUS. In: VaMoS, pp. 83\u201391 (2012)","DOI":"10.1145\/2110147.2110157"},{"issue":"1","key":"39_CR28","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.\u00a032(1), 57\u201395 (1987)","journal-title":"Artif. Intell."},{"key":"39_CR29","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.\u00a06695, pp. 174\u2013187. Springer, Heidelberg (2011)"},{"issue":"3","key":"39_CR30","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s10817-007-9076-z","volume":"39","author":"S. Schlobach","year":"2007","unstructured":"Schlobach, S., Huang, Z., Cornet, R., van Harmelen, F.: Debugging incoherent terminologies. J. Autom. Reasoning\u00a039(3), 317\u2013349 (2007)","journal-title":"J. Autom. Reasoning"},{"key":"39_CR31","unstructured":"Soh, T., Inoue, K.: Identifying necessary reactions in metabolic pathways by minimal model generation. In: ECAI, pp. 277\u2013282 (2010)"},{"key":"39_CR32","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\u00a0fast. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 291\u2013304. Springer, Heidelberg (2008)"},{"key":"39_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1007\/978-3-642-33558-7_49","volume-title":"Principles and Practice of Constraint Programming","author":"S. Wieringa","year":"2012","unstructured":"Wieringa, S.: Understanding, improving and parallelizing MUS finding using model rotation. In: Milano, M. (ed.) CP 2012. LNCS, vol.\u00a07514, pp. 672\u2013687. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,30]],"date-time":"2020-07-30T06:55:13Z","timestamp":1596092113000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}