{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T02:11:15Z","timestamp":1794449475822,"version":"4.9.1"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642390708","type":"print"},{"value":"9783642390715","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39071-5_21","type":"book-chapter","created":{"date-parts":[[2013,6,23]],"date-time":"2013-06-23T21:23:17Z","timestamp":1372022597000},"page":"276-292","source":"Crossref","is-referenced-by-count":25,"title":["Factoring Out Assumptions to Speed Up MUS Extraction"],"prefix":"10.1007","author":[{"given":"Jean-Marie","family":"Lagniez","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"issue":"4","key":"21_CR2","first-page":"543","volume":"89","author":"N. E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. ENTCS\u00a089(4), 543\u2013560 (2003)","journal-title":"ENTCS"},{"key":"21_CR3","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style finite model finding. In: Proc. CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (2003)"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: 4. In: Conflict-Driven Clause Learning SAT Solvers. Frontiers in Artificial Intel. and Applications, vol.\u00a0185, pp. 131\u2013153. IOS Press (February 2009)","DOI":"10.3233\/978-1-58603-929-5-131"},{"issue":"2","key":"21_CR5","doi-asserted-by":"publisher","first-page":"97","DOI":"10.3233\/AIC-2012-0523","volume":"25","author":"A. Belov","year":"2012","unstructured":"Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun.\u00a025(2), 97\u2013116 (2012)","journal-title":"AI Commun."},{"key":"21_CR6","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: Extracting MUSes. In: Proc. ECAI 2006. Frontiers in Artificial Intel. and Applications, vol.\u00a0141, pp. 387\u2013391. IOS Press (2006)"},{"key":"21_CR7","unstructured":"Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Proc. FMCAD 2010, pp. 221\u2013229. IEEE (2010)"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-21581-0_15","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"V. Ryvchin","year":"2011","unstructured":"Ryvchin, V., Strichman, O.: Faster extraction of high-level minimal unsatisfiable cores. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 174\u2013187. Springer, Heidelberg (2011)"},{"key":"21_CR9","unstructured":"Belov, A., Marques-Silva, J.: Accelerating MUS extraction with recursive model rotation. In: Proc. FMCAD 2011, pp. 37\u201340. FMCAD (2011)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-36742-7_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Belov","year":"2013","unstructured":"Belov, A., J\u00e4rvisalo, M., Marques-Silva, J.: Formula preprocessing in MUS extraction. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 108\u2013123. Springer, Heidelberg (2013)"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11814948_25","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"Z. Fu","year":"2006","unstructured":"Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 252\u2013265. Springer, Heidelberg (2006)"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Andraus, Z.S., Liffiton, M.H., Sakallah, K.A.: Refinement strategies for verification methods based on datapath abstraction. In: Proc. ASP-DAC 2006, pp. 19\u201324. IEEE (2006)","DOI":"10.1109\/ASPDAC.2006.1594639"},{"key":"21_CR13","unstructured":"Marques-Silva, J., Planes, J.: On using unsatisfiability for solving maximum satisfiability. CoRR abs\/0712.1097 (2007)"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-04772-5_40","volume-title":"Computer Aided Systems Theory - EUROCAST 2009","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Effective bit-width and under-approximation. In: Moreno-D\u00edaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) EUROCAST 2009. LNCS, vol.\u00a05717, pp. 304\u2013311. Springer, Heidelberg (2009)"},{"key":"21_CR15","unstructured":"E\u00e9n, N., Mishchenko, A., Amla, N.: A single-instance incremental SAT formulation of proof - and counterexample - based abstraction. In: Proc. FMCAD 2010, pp. 181\u2013188 (2010)"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"N\u00f6hrer, A., Biere, A., Egyed, A.: Managing SAT inconsistencies with HUMUS. In: Proc. VaMoS 2012, pp. 83\u201391. ACM (2012)","DOI":"10.1145\/2110147.2110157"},{"issue":"15","key":"21_CR17","first-page":"1277","volume":"174","author":"J. Huang","year":"2010","unstructured":"Huang, J.: Extended clause learning. AI\u00a0174(15), 1277\u20131284 (2010)","journal-title":"AI"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning SAT solvers. In: Proc. AAAI 2010 (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-31612-8_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A. Nadel","year":"2012","unstructured":"Nadel, A., Ryvchin, V.: Efficient SAT solving under assumptions. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 242\u2013255. Springer, Heidelberg (2012)"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Goldberg, E.I., Novikov, Y.: BerkMin: A fast and robust Sat-solver. In: Proc. DATE 2002, pp. 142\u2013149. IEEE (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"21_CR21","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proc. IJCAI 2009, pp. 399\u2013404. Morgan Kaufmann (2009)"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-21581-0_16","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"G. Audemard","year":"2011","unstructured":"Audemard, G., Lagniez, J.-M., Mazure, B., Sa\u00efs, L.: On freezing and reactivating learnt clauses. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 188\u2013200. Springer, Heidelberg (2011)"},{"key":"21_CR23","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: Proc. ICCAD 2001, pp. 279\u2013285 (2001)"},{"key":"21_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-02777-2_23","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"N. S\u00f6rensson","year":"2009","unstructured":"S\u00f6rensson, N., Biere, A.: Minimizing learned clauses. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 237\u2013243. Springer, Heidelberg (2009)"},{"key":"21_CR25","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: Proc. DAC 2004, pp. 518\u2013523. ACM (2004)","DOI":"10.1145\/996566.996710"},{"issue":"1-3","key":"21_CR26","first-page":"99","volume":"6","author":"G. Chu","year":"2009","unstructured":"Chu, G., Harwood, A., Stuckey, P.J.: Cache conscious data structures for boolean satisfiability solvers. JSAT\u00a06(1-3), 99\u2013120 (2009)","journal-title":"JSAT"},{"key":"21_CR27","unstructured":"Gomes, C.P., Selman, B., Kautz, H.A.: Boosting combinatorial search through randomization. In: Proc. AAAI\/IAAI 1998, pp. 431\u2013437 (1998)"},{"key":"21_CR28","unstructured":"Huang, J.: The effect of restarts on the effectiveness of clause learning. In: Proc. IJCAI 2007 (2007)"},{"key":"21_CR29","unstructured":"Pipatsrisawat, K., Darwiche, A.: RSat!2.0: SAT solver description. Technical Report Technical Report D\u2013153, Automated Reasoning Group, Comp.\u00a0Scienc.\u00a0Dept., UCLA (2007)"},{"issue":"2-4","key":"21_CR30","first-page":"75","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: Picosat essentials. JSAT\u00a04(2-4), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"21_CR31","doi-asserted-by":"crossref","unstructured":"Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. Information Processing Letters 47 (1993)","DOI":"10.1016\/0020-0190(93)90029-9"},{"key":"21_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-79719-7_4","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"A. Biere","year":"2008","unstructured":"Biere, A.: Adaptive restart strategies for conflict driven SAT solvers. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 28\u201333. Springer, Heidelberg (2008)"},{"key":"21_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-79719-7_25","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"V. Ryvchin","year":"2008","unstructured":"Ryvchin, V., Strichman, O.: Local restarts. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 271\u2013276. Springer, Heidelberg (2008)"},{"key":"21_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-642-33558-7_11","volume-title":"Principles and Practice of Constraint Programming","author":"G. Audemard","year":"2012","unstructured":"Audemard, G., Simon, L.: Refining restarts strategies for SAT and UNSAT. In: Milano, M. (ed.) CP 2012. LNCS, vol.\u00a07514, pp. 118\u2013126. Springer, Heidelberg (2012)"},{"key":"21_CR35","unstructured":"Biere, A.: Lingeling and friends at the SAT Competition 2011. FMV Report Series Technical Report 11\/1, Johannes Kepler University, Linz, Austria (2011)"},{"issue":"4","key":"21_CR36","first-page":"133","volume":"7","author":"P. van der Tak","year":"2011","unstructured":"van der Tak, P., Ramos, A., Heule, M.: Reusing the assignment trail in CDCL solvers. JSAT\u00a07(4), 133\u2013138 (2011)","journal-title":"JSAT"},{"key":"21_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-31612-8_20","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A. Nadel","year":"2012","unstructured":"Nadel, A., Ryvchin, V., Strichman, O.: Preprocessing in incremental SAT. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 256\u2013269. Springer, Heidelberg (2012)"},{"key":"21_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M. J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 355\u2013370. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2013"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39071-5_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T04:49:48Z","timestamp":1780980588000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-39071-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642390708","9783642390715"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39071-5_21","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-642-39071-5","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}