{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T22:01:04Z","timestamp":1757541664663},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797180"},{"type":"electronic","value":"9783540797197"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79719-7_18","type":"book-chapter","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T08:04:57Z","timestamp":1210061097000},"page":"182-195","source":"Crossref","is-referenced-by-count":13,"title":["Searching for Autarkies to Trim Unsatisfiable Clause Sets"],"prefix":"10.1007","author":[{"given":"Mark","family":"Liffiton","sequence":"first","affiliation":[]},{"given":"Karem","family":"Sakallah","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Andraus, Z.S., Liffiton, M.H., Sakallah, K.A.: Refinement strategies for verification methods based on datapath abstraction. In: Proceedings of the 2006 conference on Asia South Pacific design automation (ASP-DAC 2006), pp. 19\u201324 (2006)","DOI":"10.1145\/1118299.1118306"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"18_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. Journal of Experimental and Theoretical Artificial Intelligence\u00a015, 25\u201346 (2003)","journal-title":"Journal of Experimental and Theoretical Artificial Intelligence"},{"issue":"7","key":"18_CR4","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"3","key":"18_CR5","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"18_CR6","series-title":"Lecture Notes in Artificial Intelligence","first-page":"36","volume-title":"AI 2006: Advances in Artificial Intelligence","author":"N. Dershowitz","year":"2006","unstructured":"Dershowitz, N., Hanna, Z., Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. In: Sattar, A., Kang, B.-h. (eds.) AI 2006. LNCS (LNAI), vol.\u00a04304, pp. 36\u201341. Springer, Heidelberg (2006)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"18_CR8","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: 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 2007), January 2007, vol.\u00a02, pp. 2300\u20132305 (2007)"},{"issue":"3","key":"18_CR9","doi-asserted-by":"publisher","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.: Local-search extraction of MUSes. Constraints\u00a012(3), 325\u2013344 (2007)","journal-title":"Constraints"},{"issue":"1-3","key":"18_CR10","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0166-218X(00)00262-6","volume":"107","author":"O. Kullmann","year":"2000","unstructured":"Kullmann, O.: Investigations on autark assignments. Discrete Applied Mathematics\u00a0107(1-3), 99\u2013137 (2000)","journal-title":"Discrete Applied Mathematics"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Kullmann, O.: On the use of autarkies for satisfiability decision. In: LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT-2001). Electronic Notes in Discrete Mathematics, vol.\u00a09, pp. 231\u2013253 (2001)","DOI":"10.1016\/S1571-0653(04)00325-7"},{"key":"18_CR12","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.\u00a04121, pp. 22\u201335. Springer, Heidelberg (2006)"},{"issue":"1","key":"18_CR13","doi-asserted-by":"publisher","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.: Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning\u00a040(1), 1\u201333 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1007\/11499107_40","volume-title":"Theory and Applications of Satisfiability Testing","author":"M.N. Mneimneh","year":"2005","unstructured":"Mneimneh, M.N., Lynce, I., Andraus, Z.S., Silva, J.P.M., Sakallah, K.A.: A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 467\u2013474. Springer, Heidelberg (2005)"},{"issue":"3","key":"18_CR15","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0166-218X(85)90050-2","volume":"10","author":"B. Monien","year":"1985","unstructured":"Monien, B., Speckenmeyer, E.: Solving satisfiability in less than 2 n steps. Discrete Applied Mathematics\u00a010(3), 287\u2013295 (1985)","journal-title":"Discrete Applied Mathematics"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Oh, Y., Mneimneh, M.N., Andraus, Z.S., Sakallah, K.A., Markov, I.L.: AMUSE: a minimally-unsatisfiable subformula extractor. In: Proceedings of the 41st Annual Conference on Design Automation (DAC 2004), pp. 518\u2013523 (2004)","DOI":"10.1145\/996566.996710"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Safarpour, S., Liffiton, M., Mangassarian, H., Veneris, A., Sakallah, K.: Improved design debugging using maximum satisfiability. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD 2007), November 2007, pp. 13\u201319 (2007)","DOI":"10.1109\/FMCAD.2007.4401977"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"C. Sinz","year":"2005","unstructured":"Sinz, C.: Towards an optimal CNF encoding of Boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol.\u00a03709, pp. 827\u2013831. Springer, Heidelberg (2005)"},{"issue":"1","key":"18_CR19","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. Artificial Intelligence for Engineering Design, Analysis and Manufacturing\u00a017(1), 75\u201397 (2003)","journal-title":"Artificial Intelligence for Engineering Design, Analysis and Manufacturing"},{"issue":"2","key":"18_CR20","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1023\/A:1006143621319","volume":"23","author":"A. Gelder Van","year":"1999","unstructured":"Van Gelder, A.: Autarky pruning in propositional model elimination reduces failure redundancy. Journal of Automated Reasoning\u00a023(2), 137\u2013193 (1999)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","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 \u2013 SAT 2008"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79719-7_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:29:11Z","timestamp":1619522951000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79719-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797180","9783540797197"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79719-7_18","relation":{},"subject":[]}}