{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T06:17:57Z","timestamp":1768457877925,"version":"3.49.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319092836","type":"print"},{"value":"9783319092843","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09284-3_5","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T09:43:21Z","timestamp":1404294201000},"page":"48-57","source":"Crossref","is-referenced-by-count":14,"title":["MUS Extraction Using Clausal Proofs"],"prefix":"10.1007","author":[{"given":"Anton","family":"Belov","sequence":"first","affiliation":[]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-642-39799-8_39","volume-title":"Computer Aided Verification","author":"J. Marques-Silva","year":"2013","unstructured":"Marques-Silva, J., Janota, M., Belov, A.: Minimal sets over monotone predicates in boolean formulae. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 592\u2013607. Springer, Heidelberg (2013)"},{"issue":"2","key":"5_CR2","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":"5_CR3","doi-asserted-by":"crossref","unstructured":"Nadel, A., Ryvchin, V., Strichman, O.: Efficient MUS extraction with resolution. In: [24], pp.197\u2013200","DOI":"10.1109\/FMCAD.2013.6679410"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Audemard, G., Lagniez, J.M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: Application to MUS extraction, In: [25], pp. 309\u2013317","DOI":"10.1007\/978-3-642-39071-5_23"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Lagniez, J.M., Biere, A.: Factoring out assumptions to speed up MUS extraction. In: [25], pp. 276\u2013292","DOI":"10.1007\/978-3-642-39071-5_21"},{"key":"5_CR6","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.\u00a04121, pp. 36\u201341. Springer, Heidelberg (2006)"},{"key":"5_CR7","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: DATE, pp. 10880\u201310885. IEEE Computer Society (2003)"},{"key":"5_CR8","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":"5_CR9","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-36742-7_10"},{"key":"5_CR10","unstructured":"Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE, pp. 10886\u201310891 (2003)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.: Trimming while checking clausal proofs, In: [24], pp. 181\u2013188","DOI":"10.1109\/FMCAD.2013.6679408"},{"issue":"3","key":"5_CR12","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. J. ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"5_CR14","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (2009)"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Van Gelder, A.: Verifying RUP proofs of propositional unsatisfiability. In: ISAIM (2008)","DOI":"10.1007\/978-3-540-72788-0_31"},{"issue":"1","key":"5_CR16","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":"5_CR17","unstructured":"Nadel, A.: Boosting minimal unsatisfiable core extraction. In: FMCAD, pp. 121\u2013128 (October 2010)"},{"key":"5_CR18","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)"},{"key":"5_CR19","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-21581-0_14"},{"key":"5_CR20","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"},{"issue":"4","key":"5_CR21","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."},{"key":"5_CR22","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI, pp. 399\u2013404 (2009)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/11814948_8","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"T. Jussila","year":"2006","unstructured":"Jussila, T., Sinz, C., Biere, A.: Extended resolution proofs for symbolic SAT solving with quantification. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 54\u201360. Springer, Heidelberg (2006)"},{"key":"5_CR24","unstructured":"Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23. IEEE (2013)"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2013","year":"2013","unstructured":"J\u00e4rvisalo, M., Van Gelder, A. (eds.): SAT 2013. LNCS, vol.\u00a07962. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09284-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:52:06Z","timestamp":1746291126000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09284-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319092836","9783319092843"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}