{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T16:58:26Z","timestamp":1760029106871},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2008,8,5]],"date-time":"2008-08-05T00:00:00Z","timestamp":1217894400000},"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":[[2009,12]]},"DOI":"10.1007\/s10601-008-9058-8","type":"journal-article","created":{"date-parts":[[2008,8,4]],"date-time":"2008-08-04T08:36:26Z","timestamp":1217838986000},"page":"415-442","source":"Crossref","is-referenced-by-count":27,"title":["A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas"],"prefix":"10.1007","volume":"14","author":[{"given":"Mark","family":"Liffiton","sequence":"first","affiliation":[]},{"given":"Maher","family":"Mneimneh","sequence":"additional","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","published-online":{"date-parts":[[2008,8,5]]},"reference":[{"issue":"2","key":"9058_CR1","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1016\/0097-3165(86)90060-9","volume":"43","author":"R. Aharoni","year":"1986","unstructured":"Aharoni, R., & Linial, N. (1986). Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas. Journal of Combinatorial Theory Series A, 43(2), 196\u2013204.","journal-title":"Journal of Combinatorial Theory Series A"},{"key":"9058_CR2","unstructured":"Andraus, Z. S., Liffiton, M. H., & Sakallah, K. A. (2006). Refinement strategies for verification methods based on datapath abstraction. In Proceedings of the 2006 conference on Asia South Pacific design automation (ASP-DAC\u201906) (pp. 19\u201324)."},{"key":"9058_CR3","unstructured":"Andraus, Z. S., Liffiton, M. H., & Sakallah, K. A. (2007). CEGAR-based formal hardware verification: A case study. Technical Report CSE-TR-531-07, University of Michigan."},{"key":"9058_CR4","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), LNCS (Vol. 3350, pp. 174\u2013186).","DOI":"10.1007\/978-3-540-30557-6_14"},{"key":"9058_CR5","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1080\/0952813021000026795","volume":"15","author":"E. Birnbaum","year":"2003","unstructured":"Birnbaum, E., & Lozinskii, E. L. (2003). Consistent subsets of inconsistent systems: Structure and behaviour. Journal of Experimental and Theoretical Artificial Intelligence, 15, 25\u201346.","journal-title":"Journal of Experimental and Theoretical Artificial Intelligence"},{"key":"9058_CR6","doi-asserted-by":"crossref","unstructured":"Bruni, R., & Sassano, A. (2001). Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae. In LICS 2001 workshop on theory and applications of satisfiability testing (SAT-2001), Electronic Notes in Discrete Mathematics (Vol. 9, pp. 162\u2013173).","DOI":"10.1016\/S1571-0653(04)00320-8"},{"issue":"1\u20133","key":"9058_CR7","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 Applied Mathematics, 107(1\u20133), 83\u201398.","journal-title":"Discrete Applied Mathematics"},{"key":"9058_CR8","unstructured":"B\u00fcning, H. K., & Zhao, X. (2001). Minimal falsity for QBF with deficiency one. Workshop on Theory and Applications of Quantified Boolean Formulas."},{"key":"9058_CR9","doi-asserted-by":"crossref","unstructured":"Dasgupta, S., & Chandru, V. (2004). Minimal unsatisfiable sets: Classification and bounds. In M. J. Maher (Ed.), Advances in computer science\u2014ASIAN 2004, LNCS (Vol. 3321, pp. 330\u2013342). Springer.","DOI":"10.1007\/978-3-540-30502-6_24"},{"issue":"3\u20134","key":"9058_CR10","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. Annals of Mathematics and Artificial Intelligence, 23(3\u20134), 229\u2013245.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"9058_CR11","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), LNCS (Vol. 2919, pp. 502\u2013518)."},{"issue":"1","key":"9058_CR12","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., Kullmann, O., & Szeider, S. (2002). Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. Theoretical Computer Science, 289(1), 503\u2013516.","journal-title":"Theoretical Computer Science"},{"key":"9058_CR13","doi-asserted-by":"crossref","unstructured":"Gershman, R., Koifman, M., & Strichman, O. (2006). Deriving small unsatisfiable cores with dominators. In Proceedings of the 18th international conference on computer aided verification (CAV\u201906) (pp. 109\u2013122).","DOI":"10.1007\/11817963_13"},{"key":"9058_CR14","doi-asserted-by":"crossref","unstructured":"Goldberg, E., & Novikov, Y. (2003). Verification of proofs of unsatisfiability for CNF formulas. In Proceedings of the conference on design, automation, and test in Europe (DATE\u201903) (pp. 10886\u201310891).","DOI":"10.1109\/DATE.2003.1253718"},{"issue":"3","key":"9058_CR15","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/s10601-007-9019-7","volume":"12","author":"\u00c9. Gr\u00e9goire","year":"2007","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., & Piette, C. (2007). Local-search extraction of MUSes. Constraints, 12(3), 325\u2013344.","journal-title":"Constraints"},{"key":"9058_CR16","unstructured":"Hachtel, G. D., & Somenzi, F. (1996). Logic synthesis and verification algorithms. Kluwer Academic."},{"key":"9058_CR17","doi-asserted-by":"crossref","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, April.","DOI":"10.1109\/3477.752801"},{"key":"9058_CR18","doi-asserted-by":"crossref","unstructured":"Huang, J. (2005). MUP: A minimal unsatisfiability prover. In Proceedings of the 10th Asia and South Pacific design automation conference (ASP-DAC\u201905) (pp. 432\u2013437).","DOI":"10.1145\/1120725.1120907"},{"key":"9058_CR19","doi-asserted-by":"crossref","unstructured":"Jain, H., Kroening, D., Sharygina, N., & Clarke, E. (2005). Word level predicate abstraction and refinement for verifying RTL verilog. In Proceedings of the 42nd annual conference on design automation (DAC\u201905) (pp. 445\u2013450).","DOI":"10.1145\/1065579.1065697"},{"key":"9058_CR20","doi-asserted-by":"crossref","unstructured":"Kullmann, O. (2000). An application of matroid theory to the SAT problem. In 15th annual IEEE conference on computational complexity (pp. 116\u2013124), July.","DOI":"10.1109\/CCC.2000.856741"},{"key":"9058_CR21","volume-title":"Computer aided verification of coordinating processes","author":"R. P. Kurshan","year":"1994","unstructured":"Kurshan, R. P. (1994). Computer aided verification of coordinating processes. Princeton University Press, Princeton, NJ."},{"key":"9058_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), LNCS (Vol. 3569, pp. 173\u2013186).","DOI":"10.1007\/11499107_13"},{"issue":"1","key":"9058_CR23","doi-asserted-by":"crossref","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. (2008). Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning, 40(1), 1\u201333, January.","journal-title":"Journal of Automated Reasoning"},{"key":"9058_CR24","unstructured":"Lynce, I., & Marques-Silva, J. (2004). On computing minimum unsatisfiable cores. In The 7th international conference on theory and applications of satisfiability testing (SAT-2004)."},{"key":"9058_CR25","doi-asserted-by":"crossref","unstructured":"Mneimneh, M. N., Lynce, I., Andraus, Z. S., Silva, J. P. M., & Sakallah, K. A. (2005). A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. In Proceedings of the 8th international conference on theory and applications of satisfiability testing (SAT-2005), LNCS (Vol. 3569, pp. 467\u2013474).","DOI":"10.1007\/11499107_40"},{"issue":"6","key":"9058_CR26","doi-asserted-by":"crossref","first-page":"688","DOI":"10.1109\/TC.2004.1","volume":"53","author":"G. -J. Nam","year":"2004","unstructured":"Nam, G.-J., Aloul, F. A., Sakallah, K. A., & Rutenbar, R. A. (2004). A comparative study of two Boolean formulations of FPGA detailed routing constraints. IEEE Transactions on Computers, 53(6), 688\u2013696.","journal-title":"IEEE Transactions on Computers"},{"key":"9058_CR27","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 Proceedings of the 41st annual conference on design automation (DAC\u201904) (pp. 518\u2013523).","DOI":"10.1145\/996566.996710"},{"issue":"1","key":"9058_CR28","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. Journal of Computer and System Sciences, 37(1), 2\u201313.","journal-title":"Journal of Computer and System Sciences"},{"key":"9058_CR29","unstructured":"Sinz, C. (2003). SAT benchmarks from automotive product configuration. Website. http:\/\/www-sr.informatik.uni-tuebingen.de\/\u223csinz\/DC\/ ."},{"issue":"1","key":"9058_CR30","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1017\/S0890060403171065","volume":"17","author":"C. Sinz","year":"2003","unstructured":"Sinz, C., Kaiser, A., & K\u00fcchlin, W. (2003). Formal methods for the validation of automotive product configuration data. Artificial Intelligence for Engineering Design, Analysis and Manufacturing, 17(1), 75\u201397.","journal-title":"Artificial Intelligence for Engineering Design, Analysis and Manufacturing"},{"issue":"4","key":"9058_CR31","doi-asserted-by":"crossref","first-page":"656","DOI":"10.1016\/j.jcss.2004.04.009","volume":"69","author":"S. Szeider","year":"2004","unstructured":"Szeider, S. (2004). Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable. Journal of Computer and System Sciences, 69(4), 656\u2013674, December.","journal-title":"Journal of Computer and System Sciences"},{"key":"9058_CR32","doi-asserted-by":"crossref","unstructured":"Zhang, J., Li, S., & Shen, S. (2006). Extracting minimum unsatisfiable cores with a greedy genetic algorithm. In AI 2006: Advances in artificial intelligence, LNCS (Vol. 4304, pp. 847\u2013856).","DOI":"10.1007\/11941439_89"},{"key":"9058_CR33","unstructured":"Zhang, L., & Malik, S. (2003). Extracting small unsatisfiable cores from unsatisfiable Boolean formula. In The 6th international conference on theory and applications of satisfiability testing (SAT-2003)."},{"key":"9058_CR34","doi-asserted-by":"crossref","unstructured":"Zhang, L., & Malik, S. (2003). Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In Proceedings of the conference on design, automation, and test in Europe (DATE\u201903) (pp. 10880\u201310885).","DOI":"10.1109\/DATE.2003.1253717"}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-008-9058-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-008-9058-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-008-9058-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T19:14:14Z","timestamp":1559243654000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-008-9058-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,8,5]]},"references-count":34,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["9058"],"URL":"https:\/\/doi.org\/10.1007\/s10601-008-9058-8","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"value":"1383-7133","type":"print"},{"value":"1572-9354","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,8,5]]}}}