{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T06:27:14Z","timestamp":1768458434604,"version":"3.49.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030242572","type":"print"},{"value":"9783030242589","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-24258-9_15","type":"book-chapter","created":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T17:02:31Z","timestamp":1561741351000},"page":"211-221","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["On Computing the Union of MUSes"],"prefix":"10.1007","author":[{"given":"Carlos","family":"Menc\u00eda","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oliver","family":"Kullmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexey","family":"Ignatiev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,29]]},"reference":[{"key":"15_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). \n                    https:\/\/doi.org\/10.1007\/978-3-319-33954-2_3"},{"issue":"2","key":"15_CR2","doi-asserted-by":"publisher","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). \n                    https:\/\/doi.org\/10.3233\/AIC-2012-0523","journal-title":"AI Commun."},{"issue":"1","key":"15_CR3","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1080\/0952813021000026795","volume":"15","author":"E Birnbaum","year":"2003","unstructured":"Birnbaum, E., Lozinskii, E.L.: Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell. 15(1), 25\u201346 (2003). \n                    https:\/\/doi.org\/10.1080\/0952813021000026795","journal-title":"J. Exp. Theor. Artif. Intell."},{"key":"15_CR4","doi-asserted-by":"publisher","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Harrison, M.A., Banerji, R.B., Ullman, J.D. (eds.) Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, Shaker Heights, Ohio, USA, 3\u20135 May 1971. pp. 151\u2013158. ACM (1971). \n                    https:\/\/doi.org\/10.1145\/800157.805047","DOI":"10.1145\/800157.805047"},{"key":"15_CR5","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). \n                    https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"15_CR6","doi-asserted-by":"publisher","unstructured":"Gr\u00e9goire, \u00c9., Izza, Y., Lagniez, J.: Boosting MCSes enumeration. In: Lang [17], pp. 1309\u20131315. \n                    https:\/\/doi.org\/10.24963\/ijcai.2018\/182","DOI":"10.24963\/ijcai.2018\/182"},{"issue":"2","key":"15_CR7","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s10601-015-9195-9","volume":"21","author":"A Ignatiev","year":"2016","unstructured":"Ignatiev, A., Janota, M., Marques-Silva, J.: Quantified maximum satisfiability. Constraints 21(2), 277\u2013302 (2016). \n                    https:\/\/doi.org\/10.1007\/s10601-015-9195-9","journal-title":"Constraints"},{"issue":"1","key":"15_CR8","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/s10515-014-0141-7","volume":"23","author":"D Jannach","year":"2016","unstructured":"Jannach, D., Schmitz, T.: Model-based diagnosis of spreadsheet programs: a constraint-based debugging approach. Autom. Softw. Eng. 23(1), 105\u2013144 (2016). \n                    https:\/\/doi.org\/10.1007\/s10515-014-0141-7","journal-title":"Autom. Softw. Eng."},{"issue":"1","key":"15_CR9","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s10515-018-0250-9","volume":"26","author":"D Jannach","year":"2019","unstructured":"Jannach, D., Schmitz, T., Hofer, B., Schekotihin, K., Koch, P.W., Wotawa, F.: Fragment-based spreadsheet debugging. Autom. Softw. Eng. 26(1), 203\u2013239 (2019). \n                    https:\/\/doi.org\/10.1007\/s10515-018-0250-9","journal-title":"Autom. Softw. Eng."},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-642-23786-7_32","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"M Janota","year":"2011","unstructured":"Janota, M., Marques-Silva, J.: On deciding MUS membership with QBF. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 414\u2013428. Springer, Heidelberg (2011). \n                    https:\/\/doi.org\/10.1007\/978-3-642-23786-7_32"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-22110-1_40","volume-title":"Computer Aided Verification","author":"M Jose","year":"2011","unstructured":"Jose, M., Majumdar, R.: Bug-assist: assisting fault localization in ANSI-C programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 504\u2013509. Springer, Heidelberg (2011). \n                    https:\/\/doi.org\/10.1007\/978-3-642-22110-1_40"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2011, San Jose, CA, USA, 4\u20138 June 2011. pp. 437\u2013446. ACM (2011). \n                    https:\/\/doi.org\/10.1145\/1993498.1993550","DOI":"10.1145\/1993498.1993550"},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Kleine B\u00fcning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 339\u2013401. IOS Press (2009). \n                    https:\/\/doi.org\/10.3233\/978-1-58603-929-5-339","DOI":"10.3233\/978-1-58603-929-5-339"},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Kullmann, O.: An application of matroid theory to the SAT problem. In: Proceedings of the 15th Annual IEEE Conference on Computational Complexity, Florence, Italy, 4\u20137 July 2000, p. 116. IEEE Computer Society (2000). \n                    https:\/\/doi.org\/10.1109\/CCC.2000.856741","DOI":"10.1109\/CCC.2000.856741"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/11814948_4","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"O Kullmann","year":"2006","unstructured":"Kullmann, O., Lynce, I., Marques-Silva, J.: Categorisation of clauses in conjunctive normal forms: minimally unsatisfiable sub-clause-sets and the lean kernel. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 22\u201335. Springer, Heidelberg (2006). \n                    https:\/\/doi.org\/10.1007\/11814948_4"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-319-24318-4_11","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"O Kullmann","year":"2015","unstructured":"Kullmann, O., Marques-Silva, J.: Computing maximal autarkies with few and simple oracle queries. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 138\u2013155. Springer, Cham (2015). \n                    https:\/\/doi.org\/10.1007\/978-3-319-24318-4_11"},{"key":"15_CR17","unstructured":"Lang, J. (ed.): Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. IJCAI 2018, Stockholm, Sweden, 13\u201319 July 2018 (2018). \n                    www.ijcai.org"},{"issue":"2","key":"15_CR18","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). \n                    https:\/\/doi.org\/10.1016\/j.artint.2004.11.002","journal-title":"Artif. Intell."},{"issue":"2","key":"15_CR19","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). \n                    https:\/\/doi.org\/10.1007\/s10601-015-9183-0","journal-title":"Constraints"},{"key":"15_CR20","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 Liffiton","year":"2008","unstructured":"Liffiton, M., Sakallah, K.: Searching for autarkies to trim unsatisfiable clause sets. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 182\u2013195. Springer, Heidelberg (2008). \n                    https:\/\/doi.org\/10.1007\/978-3-540-79719-7_18"},{"key":"15_CR21","doi-asserted-by":"publisher","unstructured":"Marques-Silva, J., Ignatiev, A., Morgado, A., Manquinho, V.M., Lynce, I.: Efficient autarkies. In: Schaub, T., Friedrich, G., O\u2019Sullivan, B. (eds.) ECAI 2014\u201321st European Conference on Artificial Intelligence, 18\u201322 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems (PAIS 2014). Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 603\u2013608. IOS Press (2014). \n                    https:\/\/doi.org\/10.3233\/978-1-61499-419-0-603","DOI":"10.3233\/978-1-61499-419-0-603"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/978-3-319-40970-2_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"C Menc\u00eda","year":"2016","unstructured":"Menc\u00eda, C., Ignatiev, A., Previti, A., Marques-Silva, J.: MCS extraction with sublinear oracle queries. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 342\u2013360. Springer, Cham (2016). \n                    https:\/\/doi.org\/10.1007\/978-3-319-40970-2_21"},{"key":"15_CR23","unstructured":"Menc\u00eda, C., Previti, A., Marques-Silva, J.: Literal-based MCS extraction. In: Yang, Q., Wooldridge, M.J. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. IJCAI 2015, 25\u201331 July 2015, Buenos Aires, Argentina, pp. 1973\u20131979. AAAI Press (2015). \n                    http:\/\/ijcai.org\/Abstract\/15\/280"},{"key":"15_CR24","doi-asserted-by":"publisher","unstructured":"Narodytska, N., Bj\u00f8rner, N., Marinescu, M., Sagiv, M.: Core-guided minimal correction set and core enumeration. In: Lang [17], pp. 1353\u20131361. \n                    https:\/\/doi.org\/10.24963\/ijcai.2018\/188","DOI":"10.24963\/ijcai.2018\/188"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-66263-3_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"A Previti","year":"2017","unstructured":"Previti, A., Menc\u00eda, C., J\u00e4rvisalo, M., Marques-Silva, J.: Improving MCS enumeration via caching. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 184\u2013194. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-66263-3_12"},{"key":"15_CR26","unstructured":"Previti, A., Menc\u00eda, C., J\u00e4rvisalo, M., Marques-Silva, J.: Premise set caching for enumerating minimal correction subsets. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI 2018), the 30th innovative Applications of Artificial Intelligence (IAAI 2018), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI 2018), New Orleans, Louisiana, USA, 2\u20137 February 2018. pp. 6633\u20136640. AAAI Press (2018). \n                    https:\/\/www.aaai.org\/ocs\/index.php\/AAAI\/AAAI18\/paper\/view\/17328"},{"issue":"1","key":"15_CR27","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). \n                    https:\/\/doi.org\/10.1016\/0004-3702(87)90062-2","journal-title":"Artif. Intell."},{"key":"15_CR28","doi-asserted-by":"publisher","unstructured":"Safarpour, S., Mangassarian, H., Veneris, A.G., Liffiton, M.H., Sakallah, K.A.: Improved design debugging using maximum satisfiability. In: Proceedings of the 7th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2007, Austin, Texas, USA, 11\u201314 November 2007, pp. 13\u201319. IEEE Computer Society (2007). \n                    https:\/\/doi.org\/10.1109\/FAMCAD.2007.26","DOI":"10.1109\/FAMCAD.2007.26"},{"issue":"3","key":"15_CR29","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 39(3), 317\u2013349 (2007). \n                    https:\/\/doi.org\/10.1007\/s10817-007-9076-z","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"15_CR30","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1017\/S0890060403171065","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). \n                    https:\/\/doi.org\/10.1017\/S0890060403171065","journal-title":"AI EDAM"},{"issue":"10","key":"15_CR31","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.G., Ali, M.F., Viglas, A.: Fault diagnosis and logic debugging using Boolean satisfiability. IEEE Trans. CAD Integr. Circ. Syst. 24(10), 1606\u20131621 (2005). \n                    https:\/\/doi.org\/10.1109\/TCAD.2005.852031","journal-title":"IEEE Trans. CAD Integr. Circ. Syst."},{"key":"15_CR32","doi-asserted-by":"publisher","unstructured":"Stuckey, P.J., Sulzmann, M., Wazny, J.: Interactive type debugging in Haskell. In: Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2003, Uppsala, Sweden, 28 August 2003. pp. 72\u201383. ACM (2003). \n                    https:\/\/doi.org\/10.1145\/871895.871903","DOI":"10.1145\/871895.871903"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2019"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-24258-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,31]],"date-time":"2019-07-31T13:05:56Z","timestamp":1564578356000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-24258-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030242572","9783030242589"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-24258-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"29 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sat2019.tecnico.ulisboa.pt\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}