{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T21:07:53Z","timestamp":1725829673454},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243177"},{"type":"electronic","value":"9783319243184"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24318-4_3","type":"book-chapter","created":{"date-parts":[[2015,9,11]],"date-time":"2015-09-11T05:42:56Z","timestamp":1441950176000},"page":"17-32","source":"Crossref","is-referenced-by-count":0,"title":["Speeding up MUS Extraction with Preprocessing and Chunking"],"prefix":"10.1007","author":[{"given":"Valeriy","family":"Balabanov","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Ivrii","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,27]]},"reference":[{"issue":"1","key":"3_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1\u201333 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR2","unstructured":"Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20\u201323, pp. 221\u2013229 (2010)"},{"key":"3_CR3","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 (ETAPS 2013). LNCS, vol. 7795, pp. 108\u2013123. Springer, Heidelberg (2013)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-642-45221-5_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A Belov","year":"2013","unstructured":"Belov, A., Morgado, A., Marques-Silva, J.: SAT-based preprocessing for MaxSAT. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 96\u2013111. Springer, Heidelberg (2013)"},{"key":"3_CR5","unstructured":"Belov, A., Marques-Silva, J.: Generalizing redundancy in propositional logic: Foundations and hitting sets duality. CoRR, abs\/1207.1257 (2012)"},{"key":"3_CR6","unstructured":"Belov, A., Marques-Silva, J.: Accelerating MUS extraction with recursive model rotation. In: International Conference on Formal Methods in Computer-Aided Design, FMCAD 2011, Austin, TX, USA, October 30 - November 02, 2011, pp. 37\u201340 (2011)"},{"issue":"3\/4","key":"3_CR7","first-page":"123","volume":"8","author":"A Belov","year":"2012","unstructured":"Belov, A., Marques-Silva, J.: Muser2: An efficient MUS extractor. JSAT 8(3\/4), 123\u2013128 (2012)","journal-title":"JSAT"},{"key":"3_CR8","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. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"3_CR9","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. 6695, pp. 174\u2013187. Springer, Heidelberg (2011)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-39071-5_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"J-M Lagniez","year":"2013","unstructured":"Lagniez, J.-M., Biere, A.: Factoring out assumptions to speed up MUS extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 276\u2013292. Springer, Heidelberg (2013)"},{"key":"3_CR11","first-page":"27","volume":"9","author":"A Nadel","year":"2014","unstructured":"Nadel, A., Ryvchin, V., Strichman, O.: Accelerated deletion-based extraction of minimal unsatisfiable cores. JSAT 9, 27\u201351 (2014)","journal-title":"JSAT"},{"key":"3_CR12","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. 5584, pp. 237\u2013243. Springer, Heidelberg (2009)"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-33558-7_14","volume-title":"Principles and Practice of Constraint Programming","author":"A Belov","year":"2012","unstructured":"Belov, A., Janota, M., Lynce, I., Marques-Silva, J.: On computing minimal equivalent subformulas. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 158\u2013174. Springer, Heidelberg (2012)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/978-3-319-09284-3_5","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"A Belov","year":"2014","unstructured":"Belov, A., Heule, M.J.H., Marques-Silva, J.: MUS extraction using clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 48\u201357. Springer, Heidelberg (2014)"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-642-21581-0_14","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"J Marques-Silva","year":"2011","unstructured":"Marques-Silva, J., Lynce, I.: On improving MUS extraction algorithms. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 159\u2013173. Springer, Heidelberg (2011)"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11814948_5","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"N Dershowitz","year":"2006","unstructured":"Dershowitz, N., Hanna, Z., Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 36\u201341. Springer, Heidelberg (2006)"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-31612-8_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A Belov","year":"2012","unstructured":"Belov, A., Ivrii, A., Matsliah, A., Marques-Silva, J.: On efficient computation of variable MUSes. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 298\u2013311. Springer, Heidelberg (2012)"},{"key":"3_CR18","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11\u201317, 2009, pp. 399\u2013404 (2009)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing -- SAT 2015"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24318-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T23:13:52Z","timestamp":1559258032000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24318-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243177","9783319243184"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24318-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}