{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T04:19:57Z","timestamp":1780633197159,"version":"3.54.1"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,3,22]],"date-time":"2015-03-22T00:00:00Z","timestamp":1426982400000},"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":["Constraints"],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1007\/s10601-015-9183-0","type":"journal-article","created":{"date-parts":[[2015,3,21]],"date-time":"2015-03-21T03:57:15Z","timestamp":1426910235000},"page":"223-250","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":84,"title":["Fast, flexible MUS enumeration"],"prefix":"10.1007","volume":"21","author":[{"given":"Mark H.","family":"Liffiton","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Previti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ammar","family":"Malik","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,3,22]]},"reference":[{"key":"9183_CR1","doi-asserted-by":"crossref","unstructured":"Andraus, Z.S., Liffiton, M.H., & Sakallah, K.A. (2008). Reveal: A formal verification tool for Verilog designs. In Proceedings of 15th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-2008). (pp. 343\u2013352).","DOI":"10.1007\/978-3-540-89439-1_25"},{"key":"9183_CR2","doi-asserted-by":"crossref","unstructured":"Bailey, J., & Stuckey, P.J. (2005). Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages (PADL\u201905) of LNCS, Vol. 3350. (pp. 174\u2013186).","DOI":"10.1007\/978-3-540-30557-6_14"},{"key":"9183_CR3","doi-asserted-by":"crossref","first-page":"123","DOI":"10.3233\/SAT190094","volume":"8","author":"A Belov","year":"2012","unstructured":"Belov, A., & Marques-Silva, J. (2012). MUSer2: An efficient MUS extractor. Journal on Satisfiability, Boolean Modeling and Computation, 8, 123\u2013128.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9183_CR4","volume-title":"Hypergraphs of North-Holland Mathematical Library, Vol. 45","author":"C Berge","year":"1989","unstructured":"Berge, C. (1989). Hypergraphs of North-Holland Mathematical Library. Vol. 45. Amsterdam: North-Holland Publishing Co."},{"key":"9183_CR5","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., & Sebastiani, R. (2013). A modular approach to MaxSAT modulo theories. In Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT-2013). (pp. 150\u2013165).","DOI":"10.1007\/978-3-642-39071-5_12"},{"key":"9183_CR6","doi-asserted-by":"crossref","unstructured":"Davies, J., & Bacchus, F. (2011). Solving MAXSAT by solving a sequence of simpler SAT instances. In Principles and Practice of Constraint Programming (CP 2011). (pp. 225\u2013239): Springer.","DOI":"10.1007\/978-3-642-23786-7_19"},{"issue":"1","key":"9183_CR7","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(87)90063-4","volume":"32","author":"J de Kleer","year":"1987","unstructured":"de Kleer, J., & Williams, B.C. (1987). Diagnosing multiple faults. Artificial Intelligence, 32(1), 97\u2013130.","journal-title":"Artificial Intelligence"},{"key":"9183_CR8","doi-asserted-by":"crossref","unstructured":"Garc\u00eda de la Banda, M.J., Stuckey, P.J., & Wazny, J. (2003). Finding all minimal unsatisfiable subsets. In Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming (PPDP\u201903). (pp. 32\u201343).","DOI":"10.1145\/888251.888256"},{"issue":"4","key":"9183_CR9","doi-asserted-by":"crossref","first-page":"395","DOI":"10.3233\/AIC-130575","volume":"26","author":"E Di Rosa","year":"2013","unstructured":"Di Rosa, E., & Giunchiglia, E. (2013). Combining approaches for solving satisfiability problems with qualitative preferences. AI Communications, 26(4), 395\u2013408.","journal-title":"AI Communications"},{"key":"9183_CR10","unstructured":"E\u00e9n, N., & S\u00f6rensson, N. (2003). An extensible SAT-solver. In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT-2003) of LNCS, Vol. 2919. (pp. 502\u2013518)."},{"issue":"3","key":"9183_CR11","doi-asserted-by":"crossref","first-page":"618","DOI":"10.1006\/jagm.1996.0062","volume":"21","author":"ML Fredman","year":"1996","unstructured":"Fredman, M. L., & Khachiyan, L. (1996). On the complexity of dualization of monotone disjunctive normal forms. Journal of Algorithms, 21(3), 618\u2013628.","journal-title":"Journal of Algorithms"},{"key":"9183_CR12","doi-asserted-by":"crossref","unstructured":"Gasca, R. M., Valle, C. D., L\u00f3pez, M. T. G., & Ceballos, R. (2007). NMUS: Structural analysis for improving the derivation of all MUSes in overconstrained numeric CSPs. In Current Topics in Artificial Intelligence, 12th Conference of the Spanish Association for Artificial Intelligence (CAEPIA 2007) of LNCS, Vol. 4788. (pp. 160\u2013169).","DOI":"10.1007\/978-3-540-75271-4_17"},{"issue":"1","key":"9183_CR13","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1287\/ijoc.2.1.61","volume":"2","author":"J Gleeson","year":"1990","unstructured":"Gleeson, J., & Ryan, J. (1990). Identifying minimally infeasible subsytems. ORSA Journal on Computing, 2(1), 61\u201367.","journal-title":"ORSA Journal on Computing"},{"key":"9183_CR14","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., & Piette, C. (2007). Boosting a complete technique to find MSSes and MUSes thanks to a local search oracle. In Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI\u201907), Vol. 2. (pp. 2300\u20132305)."},{"issue":"2","key":"9183_CR15","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1145\/777943.777945","volume":"28","author":"D Gunopulos","year":"2003","unstructured":"Gunopulos, D., Khardon, R., Mannila, H., Saluja, S., Toivonen, H., & Sharma, R.S. (2003). Discovering all most specific sentences. ACM Transactions on Database Systems (TODS), 28(2), 140\u2013174.","journal-title":"ACM Transactions on Database Systems (TODS)"},{"issue":"2","key":"9183_CR16","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1109\/3477.752801","volume":"29","author":"B Han","year":"1999","unstructured":"Han, B., & Lee, S.-J. (1999). Deriving minimal conflict sets by CS-trees with mark set in diagnosis from first principles. IEEE Transactions on Systems, Man, and Cybernetics, Part B, 29(2), 281\u2013286.","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics, Part B"},{"issue":"2","key":"9183_CR17","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/0004-3702(94)90019-1","volume":"65","author":"A Hou","year":"1994","unstructured":"Hou, A. (1994). A theory of measurement in diagnosis from first principles. Artificial Intelligence, 65(2), 281\u2013328.","journal-title":"Artificial Intelligence"},{"key":"9183_CR18","unstructured":"Junker, U. (2004). QuickXplain: Preferred explanations and relaxations for over-constrained problems. In Proceedings of the 19th AAAI Conference on Artificial Intelligence (AAAI 2004). (pp. 167\u2013172)."},{"issue":"3","key":"9183_CR19","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/S0020-0190(00)00023-5","volume":"74","author":"DJ Kavvadias","year":"2000","unstructured":"Kavvadias, D.J., Sideri, M., & Stavropoulos, E.C. (2000). Generating all maximal models of a Boolean expression. Information Processing Letters, 74(3), 157\u2013162.","journal-title":"Information Processing Letters"},{"key":"9183_CR20","doi-asserted-by":"crossref","unstructured":"Kullmann, O., Lynce, I., & Marques-Silva, J. (2006). Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel. In Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT-2006) of LNCS, Vol. 4121. (pp. 22\u201335).","DOI":"10.1007\/11814948_4"},{"key":"9183_CR21","doi-asserted-by":"crossref","unstructured":"Liffiton, M. H., & Malik, A. (2013). Enumerating infeasibility: Finding multiple MUSes quickly. In Proceedings of the 10th International Conference on Integration of AI and OR Techniques in Constraint Programming (CPAIOR 2013). (pp. 160\u2013175).","DOI":"10.1007\/978-3-642-38171-3_11"},{"key":"9183_CR22","doi-asserted-by":"crossref","unstructured":"Liffiton, M. H., & Sakallah, K. A. (2005). On finding all minimally unsatisfiable subformulas. In Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT-2005) of LNCS, Vol. 3569. (pp. 173\u2013186).","DOI":"10.1007\/11499107_13"},{"issue":"1","key":"9183_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M. H., & Sakallah, K. A. (2008). Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning, 40(1), 1\u201333.","journal-title":"Journal of Automated Reasoning"},{"key":"9183_CR24","doi-asserted-by":"crossref","unstructured":"Liffiton, M. H., & Sakallah, K. A. (2009). Generalizing core-guided Max-SAT. In Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT-2009) of LNCS, Vol. 5584. (pp. 481\u2013494).","DOI":"10.1007\/978-3-642-02777-2_44"},{"key":"9183_CR25","unstructured":"Marques-Silva, J., Heras, F., Janota, M., Previti, A., & Belov, A. (2013). On computing minimal correction subsets. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI-2013). (pp. 615\u2013622): AAAI Press."},{"key":"9183_CR26","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., & Previti, A. (2014). On computing preferred MUSes and MCSes. In Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT-2014). (pp. 58\u201374): Springer.","DOI":"10.1007\/978-3-319-09284-3_6"},{"issue":"4","key":"9183_CR27","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/s10601-013-9146-2","volume":"18","author":"A Morgado","year":"2013","unstructured":"Morgado, A., Heras, F., Liffiton, M., Planes, J., & Marques-Silva, J. (2013). Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints, 18(4), 478\u2013534.","journal-title":"Constraints"},{"key":"9183_CR28","doi-asserted-by":"crossref","unstructured":"Previti, A., & Marques-Silva, J. (2013). Partial MUS enumeration. In Proceedings of the 27th AAAI Conference on Artificial Intelligence (AAAI-2013). (pp. 818\u2013825).","DOI":"10.1609\/aaai.v27i1.8657"},{"issue":"1","key":"9183_CR29","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R Reiter","year":"1987","unstructured":"Reiter, R. (1987). A theory of diagnosis from first principles. Artificial Intelligence, 32(1), 57\u201395.","journal-title":"Artificial Intelligence"},{"key":"9183_CR30","unstructured":"Stern, R. T., Kalech, M., Feldman, A., & Provan, G. M. (2012). Exploring the duality in conflict-directed model-based diagnosis. In Proceedings of the 26th AAAI Conference on Artificial Intelligence (AAAI-2012)."},{"issue":"3","key":"9183_CR31","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1016\/0377-2217(81)90177-6","volume":"8","author":"J van Loon","year":"1981","unstructured":"van Loon, J. (1981). Irreducibly inconsistent systems of linear inequalities. European Journal of Operational Research, 8(3), 283\u2013288.","journal-title":"European Journal of Operational Research"}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-015-9183-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-015-9183-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-015-9183-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,8]],"date-time":"2023-08-08T22:51:46Z","timestamp":1691535106000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-015-9183-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,22]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["9183"],"URL":"https:\/\/doi.org\/10.1007\/s10601-015-9183-0","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"value":"1383-7133","type":"print"},{"value":"1572-9354","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,22]]}}}