{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T19:45:38Z","timestamp":1725479138608},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540262763"},{"type":"electronic","value":"9783540316794"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11499107_40","type":"book-chapter","created":{"date-parts":[[2010,7,14]],"date-time":"2010-07-14T17:56:25Z","timestamp":1279130185000},"page":"467-474","source":"Crossref","is-referenced-by-count":26,"title":["A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas"],"prefix":"10.1007","author":[{"given":"Maher","family":"Mneimneh","sequence":"first","affiliation":[]},{"given":"In\u00eas","family":"Lynce","sequence":"additional","affiliation":[]},{"given":"Zaher","family":"Andraus","sequence":"additional","affiliation":[]},{"given":"Jo\u00e3o","family":"Marques-Silva","sequence":"additional","affiliation":[]},{"given":"Karem","family":"Sakallah","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"40_CR1","doi-asserted-by":"crossref","unstructured":"Bruni, R., Sassano, A.: Restoring Satisfiability or Maintaining Unsatisfiability by finding small Unsatisfiable Subformulae. Electronic Notes in Discrete Mathematics\u00a09 (2001)","DOI":"10.1016\/S1571-0653(04)00320-8"},{"key":"40_CR2","doi-asserted-by":"crossref","unstructured":"Huang, J.: MUP: A Minimal Unsatisfiability Prover. In: Proceedings of Asia South Pacific Design Automation Conference (2005)","DOI":"10.1145\/1120725.1120907"},{"key":"40_CR3","unstructured":"Liffiton, M., Andraus, Z., Sakallah, K.: From MAX-SAT to Min-UNSAT: Insights and Applications. Technical Report CSE-TR-506-05, University of Michigan (2005)"},{"key":"40_CR4","series-title":"Lecture Notes in Computer Science","first-page":"305","volume-title":"Theory and Applications of Satisfiability Testing","author":"I. Lynce","year":"2005","unstructured":"Lynce, I., Marques-Silva, J.: On Computing Minimum Unsatisfiable Cores. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 305\u2013310. Springer, Heidelberg (2005)"},{"key":"40_CR5","unstructured":"SAT benchmarks from Automotive Product Configuration, \n                    \n                      http:\/\/www-sr.informatik.unituebingen.de\/~sinz\/DC\/"},{"key":"40_CR6","unstructured":"Satzoo, \n                    \n                      http:\/\/www.cs.chalmers.se\/~een\/Satzoo\/"},{"key":"40_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_22","volume-title":"Theory and Applications of Satisfiability Testing","author":"L. Zhang","year":"2004","unstructured":"Zhang, L., Malik, S.: Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formula. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11499107_40.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T02:41:21Z","timestamp":1619491281000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11499107_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540262763","9783540316794"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/11499107_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}