{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T18:16:41Z","timestamp":1725733001594},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642390708"},{"type":"electronic","value":"9783642390715"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39071-5_11","type":"book-chapter","created":{"date-parts":[[2013,6,24]],"date-time":"2013-06-24T01:23:17Z","timestamp":1372036997000},"page":"133-149","source":"Crossref","is-referenced-by-count":2,"title":["Parallel MUS Extraction"],"prefix":"10.1007","author":[{"given":"Anton","family":"Belov","sequence":"first","affiliation":[]},{"given":"Norbert","family":"Manthey","sequence":"additional","affiliation":[]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-31612-8_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"G. Audemard","year":"2012","unstructured":"Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.-M., Piette, C.: Revisiting clause exchange in parallel SAT solving. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 200\u2013213. Springer, Heidelberg (2012)"},{"key":"11_CR2","first-page":"399","volume-title":"Proceedings of the 21st International Jont Conference on Artifical Intelligence, IJCAI 2009","author":"G. Audemard","year":"2009","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern sat solvers. In: Proceedings of the 21st International Jont Conference on Artifical Intelligence, IJCAI 2009, pp. 399\u2013404. Morgan Kaufmann Publishers Inc., San Francisco (2009)"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Belov, A., Chen, H., Mishchenko, A., Marques-Silva, J.: Core minimization in SAT-based abstraction. In: DATE (2013)","DOI":"10.7873\/DATE.2013.288"},{"issue":"2","key":"11_CR4","doi-asserted-by":"crossref","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 Communications\u00a025(2), 97\u2013116 (2012)","journal-title":"AI Communications"},{"key":"11_CR5","first-page":"123","volume":"8","author":"A. Belov","year":"2012","unstructured":"Belov, A., Marques-Silva, J.: MUSer2: An efficient MUS extractor. Journal of Satisfiability\u00a08, 123\u2013128 (2012)","journal-title":"Journal of Satisfiability"},{"key":"11_CR6","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Report Series Technical Report 10\/1, Johannes Kepler University, Linz, Austria (2010)"},{"key":"11_CR7","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (2009)"},{"key":"11_CR8","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, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"4","key":"11_CR9","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N. E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci.\u00a089(4), 543\u2013560 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1-2","key":"11_CR10","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1023\/A:1006314320276","volume":"24","author":"C.P. Gomes","year":"2000","unstructured":"Gomes, C.P., Selman, B., Crato, N., Kautz, H.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. Journal of Automated Reasoning\u00a024(1-2), 67\u2013100 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR11","first-page":"499","volume-title":"Proceedings of the 21st International Jont Conference on Artifical Intelligence","author":"Y. Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Control-based clause sharing in parallel sat solving. In: Proceedings of the 21st International Jont Conference on Artifical Intelligence, pp. 499\u2013504. Morgan Kaufmann Publishers Inc., San Francisco (2009)"},{"issue":"4","key":"11_CR12","first-page":"245","volume":"6","author":"Y. Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. JSAT\u00a06(4), 245\u2013262 (2009)","journal-title":"JSAT"},{"key":"11_CR13","unstructured":"H\u00f6lldobler, S., Manthey, N., Nguyen, V.H., Stecklina, J., Steinke, P.: A short overview on modern parallel SAT-solvers. In: Wasito, I., et al. (eds.) Proceedings of the International Conference on Advanced Computer Science and Information Systems, pp. 201\u2013206 (2011) ISBN 978-979-1421-11-9"},{"key":"11_CR14","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":"11_CR15","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. J. Autom. Reasoning\u00a040(1), 1\u201333 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.: Minimal unsatisfiability: Models, algorithms and applications. In: ISMVL, pp. 9\u201314 (2010)","DOI":"10.1109\/ISMVL.2010.11"},{"key":"11_CR17","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.\u00a06695, pp. 159\u2013173. Springer, Heidelberg (2011)"},{"issue":"5","key":"11_CR18","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques Silva","year":"1999","unstructured":"Marques Silva, J.P., Sakallah, K.A.: Grasp: A search algorithm for propositional satisfiability. IEEE Trans. Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Computers"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/s10601-012-9121-3","volume":"17","author":"R. Martins","year":"2012","unstructured":"Martins, R., Manquinho, V., Lynce, I.: An overview of parallel SAT solving. Constraints\u00a017, 304\u2013347 (2012)","journal-title":"Constraints"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. 38th Annual ACM\/IEEE Design Automation Conf. (DAC), pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"11_CR21","unstructured":"Nadel, A.: Boosting minimal unsatisfiable core extraction. In: FMCAD, pp. 121\u2013128 (October 2010)"},{"key":"11_CR22","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)"},{"issue":"1","key":"11_CR23","doi-asserted-by":"publisher","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.: The complexity of facets resolved. J. Comput. Syst. Sci.\u00a037(1), 2\u201313 (1988)","journal-title":"J. Comput. Syst. Sci."},{"key":"11_CR24","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":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-642-21581-0_26","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"A. Gelder Van","year":"2011","unstructured":"Van Gelder, A.: Generalized conflict-clause strengthening for satisfiability solvers. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 329\u2013342. Springer, Heidelberg (2011)"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1007\/978-3-642-33558-7_49","volume-title":"Principles and Practice of Constraint Programming","author":"S. Wieringa","year":"2012","unstructured":"Wieringa, S.: Understanding, improving and parallelizing MUS finding using model rotation. In: Milano, M. (ed.) CP 2012. LNCS, vol.\u00a07514, pp. 672\u2013687. Springer, Heidelberg (2012)"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-642-36742-7_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Wieringa","year":"2013","unstructured":"Wieringa, S., Heljanko, K.: Asynchronous multi-core incremental SAT solving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 139\u2013153. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2013"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39071-5_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,28]],"date-time":"2020-07-28T23:52:01Z","timestamp":1595980321000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39071-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642390708","9783642390715"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39071-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}