{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,12,21]],"date-time":"2023-12-21T05:59:42Z","timestamp":1703138382007},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T00:00:00Z","timestamp":1181347200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2007,7,13]]},"DOI":"10.1007\/s10601-007-9019-7","type":"journal-article","created":{"date-parts":[[2007,6,8]],"date-time":"2007-06-08T13:29:15Z","timestamp":1181309355000},"page":"325-344","source":"Crossref","is-referenced-by-count":31,"title":["Local-search Extraction of MUSes"],"prefix":"10.1007","volume":"12","author":[{"given":"\u00c9ric","family":"Gr\u00e9goire","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertrand","family":"Mazure","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9dric","family":"Piette","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,6,9]]},"reference":[{"key":"9019_CR1","doi-asserted-by":"crossref","unstructured":"Bailey, J., & Stuckey, P. J. (2005). Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In International Symposium on Practical Aspects of Declarative Languages (PADL\u201905), pages 174\u2013186.","DOI":"10.1007\/978-3-540-30557-6_14"},{"key":"9019_CR2","unstructured":"Boussemart, F., H\u00e9mery, F., Lecoutre, C., & Sa\u00efs, L. (2004). Boosting systematic search by weighting constraints. In European Conference on Artificial Intelligence (ECAI\u201904), pages 146\u2013150."},{"issue":"3","key":"9019_CR3","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1002\/1098-111X(200103)16:3<319::AID-INT1010>3.0.CO;2-U","volume":"16","author":"L. Brisoux","year":"2001","unstructured":"Brisoux, L., Gr\u00e9goire, \u00c9., & Sa\u00efs, L. (2001). Checking depth-limited consistency and inconsistency in knowledge-based systems. Int. J. Intell. Syst. 16(3): 333\u2013360.","journal-title":"Int. J. Intell. Syst."},{"issue":"2","key":"9019_CR4","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0166-218X(02)00399-2","volume":"130","author":"R. Bruni","year":"2003","unstructured":"Bruni, R. (2003). Approximating minimal unsatisfiable subformulae by means of adaptive core search. Discrete Appl. Math. 130(2): 85\u2013100.","journal-title":"Discrete Appl. Math."},{"issue":"1","key":"9019_CR5","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/s10472-005-0418-4","volume":"43","author":"R. Bruni","year":"2005","unstructured":"Bruni, R. (2005). On exact selection of minimally unsatisfiable subformulae. Ann. Math. Artif. Intell. 43(1): 35\u201350.","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1\u20133","key":"9019_CR6","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/S0166-218X(00)00245-6","volume":"107","author":"H.K. B\u00fcning","year":"2000","unstructured":"B\u00fcning, H. K. (2000). On subclasses of minimal unsatisfiable formulas. Discrete Appl. Math. 107(1\u20133): 83\u201398.","journal-title":"Discrete Appl. Math."},{"issue":"7","key":"9019_CR7","first-page":"394","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem proving. J. Assoc. Comput. Mach. 5(7): 394\u2013397.","journal-title":"J. Assoc. Comput. Mach."},{"issue":"3,4","key":"9019_CR8","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1023\/A:1018924526592","volume":"23","author":"G. Davydov","year":"1998","unstructured":"Davydov, G., Davydova, I., & B\u00fcning, H. K. (1998). An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF. Ann. Math. Artif. Intell. 23(3,4): 229\u2013245.","journal-title":"Ann. Math. Artif. Intell."},{"key":"9019_CR9","unstructured":"DIMACS (1993). Benchmarks on SAT. ftp:\/\/dimacs.rutgers.edu\/pub\/challenge\/-satisfiability\/ ."},{"key":"9019_CR10","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(92)90018-S","volume":"57","author":"T. Eiter","year":"1992","unstructured":"Eiter, T., & Gottlob, G. (1992). On the complexity of propositional knowledge base revision, updates and counterfactual. Artif. Intell. 57: 227\u2013270.","journal-title":"Artif. Intell."},{"issue":"1","key":"9019_CR11","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/S0304-3975(01)00337-1","volume":"289","author":"H. Fleischner","year":"2002","unstructured":"Fleischner, H., Kullman, O., & Szeider, S. (2002). Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. Theor. Comput. Sci. 289(1): 503\u2013516.","journal-title":"Theor. Comput. Sci."},{"key":"9019_CR12","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 International Joint Conference on Artificial Intelligence (IJCAI\u201907), vol.\u00a02, pages 2300\u20132305."},{"issue":"2","key":"9019_CR13","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1142\/S0218213000000082","volume":"9","author":"\u00c9 Gr\u00e9goire","year":"2000","unstructured":"Gr\u00e9goire, \u00c9., & Ansart, D. (2000). Overcoming the Christmas tree syndrome. Int. J. Artif. Intell. Tools (IJAIT) 9(2): 97\u2013111.","journal-title":"Int. J. Artif. Intell. Tools (IJAIT)"},{"key":"9019_CR14","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., & Sa\u00efs, L. (2002). Using failed local search for SAT as an oracle for tackling harder A.I. problems more efficiently. In International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA\u201902). LNCS, number 2443, pages 51\u201360. Springer."},{"key":"9019_CR15","volume-title":"Readings in Model-based Diagnosis","year":"1992","unstructured":"Hamscher, W., Console, L., & de\u00a0Kleer, J., eds. (1992) Readings in Model-based Diagnosis. San Mateo, CA: Morgan Kaufmann."},{"key":"9019_CR16","doi-asserted-by":"crossref","unstructured":"Huang, J. (2005). MUP: A minimal unsatisfiability prover. In Asia and South Pacific Design Automation Conference (ASP-DAC\u201905), pages 432\u2013437.","DOI":"10.1145\/1120725.1120907"},{"key":"9019_CR17","unstructured":"Junker, U. (2001). QuickXPlain: Conflict detection for arbitrary constraint propagation algorithms. In IJCAI\u201901 Workshop on Modelling and Solving problems with constraints (CONS-1), pages 75\u201382."},{"key":"9019_CR18","unstructured":"Kautz, H., Selman, B., & McAllester, D. (2004). Walksat in the SAT 2004 competition. In International Conference on Theory and Applications of Satisfiability Testing (SAT\u201904)."},{"key":"9019_CR19","doi-asserted-by":"crossref","unstructured":"Kullmann, O., Lynce, I., & Marques\u00a0Silva, J.\u00a0P. (2006). Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel. In International Conference on Theory and Applications of Satisfiability Testing (SAT\u201906), pages 22\u201335.","DOI":"10.1007\/11814948_4"},{"key":"9019_CR20","doi-asserted-by":"crossref","unstructured":"Liffiton, M. H., & Sakallah, K. A. (2005). On finding all minimally unsatisfiable subformulas. In International Conference on Theory and Applications of Satisfiability Testing (SAT\u201905), pages 173\u2013186.","DOI":"10.1007\/11499107_13"},{"key":"9019_CR21","unstructured":"Lynce, I., & Marques-Silva, J. (2004). On computing minimum unsatisfiable cores. In International Conference on Theory and Applications of Satisfiability Testing (SAT\u201904)."},{"key":"9019_CR22","unstructured":"Mazure, B., Sa\u00efs, L., & Gr\u00e9goire, \u00c9. (1996). A powerful heuristic to locate inconsistent kernels in knowledge-based systems. In International Conference on Information Processing and Management of Uncertainty in Knowledge-based Systems (IPMU\u201996), pages 1265\u20131269."},{"key":"9019_CR23","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1023\/A:1018999721141","volume":"22","author":"B. Mazure","year":"1998","unstructured":"Mazure, B., Sa\u00efs, L., & Gr\u00e9goire, \u00c9. (1998). Boosting complete techniques thanks to local search. Ann. Math. Artif. Intell. 22: 319\u2013322.","journal-title":"Ann. Math. Artif. Intell."},{"key":"9019_CR24","doi-asserted-by":"crossref","unstructured":"Mneimneh, M.\u00a0N., Lynce, I., Andraus, Z.\u00a0S., Marques\u00a0Silva, J.\u00a0P., & Sakallah, K.\u00a0A. (2005). A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. In International Conference on Theory and Applications of Satisfiability Testing (SAT\u201905), pages 467\u2013474.","DOI":"10.1007\/11499107_40"},{"key":"9019_CR25","doi-asserted-by":"crossref","unstructured":"Oh, Y., Mneimneh, M. N., Andraus, Z. S., Sakallah, K. A., & Markov, I. L. (2004). AMUSE: a minimally-unsatisfiable subformula extractor. In Design Automation Conference (DAC\u201904), pages 518\u2013523.","DOI":"10.1145\/996566.996710"},{"issue":"1","key":"9019_CR26","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/0022-0000(88)90042-6","volume":"37","author":"C.H. Papadimitriou","year":"1988","unstructured":"Papadimitriou, C. H., & Wolfe, D. (1988). The complexity of facets resolved. J. Comput. Syst. Sci. 37(1): 2\u201313.","journal-title":"J. Comput. Syst. Sci."},{"key":"9019_CR27","unstructured":"SATLIB (2004). Benchmarks on SAT. http:\/\/www.intellektik.informatik.tu-darmstadt.de\/SATLIB\/benchm.html ."},{"key":"9019_CR28","unstructured":"Zhang, L., & Malik, S. (2003). Extracting small unsatisfiable cores from unsatisfiable boolean formula. In International Conference on Theory and Applications of Satisfiability Testing (SAT\u201903)."}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-007-9019-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-007-9019-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-007-9019-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T19:14:13Z","timestamp":1559243653000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-007-9019-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6,9]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,7,13]]}},"alternative-id":["9019"],"URL":"https:\/\/doi.org\/10.1007\/s10601-007-9019-7","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"value":"1383-7133","type":"print"},{"value":"1572-9354","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,6,9]]}}}