{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T05:47:22Z","timestamp":1782366442829,"version":"3.54.5"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319243177","type":"print"},{"value":"9783319243184","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24318-4_8","type":"book-chapter","created":{"date-parts":[[2015,9,11]],"date-time":"2015-09-11T01:42:56Z","timestamp":1441935776000},"page":"88-103","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Mining Backbone Literals in Incremental SAT"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Ivrii","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vadim","family":"Ryvchin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ofer","family":"Strichman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,10,27]]},"reference":[{"key":"8_CR1","unstructured":"HaifaMUC. http:\/\/ie.technion.ac.il\/ofers\/haifasolvers\/"},{"issue":"3","key":"8_CR2","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-010-0167-5","volume":"13","author":"O Bar-Ilan","year":"2011","unstructured":"Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Reducing the size of resolution proofs in linear time. STTT 13(3), 263\u2013272 (2011)","journal-title":"STTT"},{"issue":"1\/2","key":"8_CR3","doi-asserted-by":"publisher","first-page":"123","DOI":"10.3233\/SAT190094","volume":"8","author":"A Belov","year":"2012","unstructured":"Belov, A., Marques-Silva, J.: MUSer2: An efficient MUS extractor. J. on Satisfiability, Boolean Modeling and Computation (JSAT) 8(1\/2), 123\u2013128 (2012)","journal-title":"J. on Satisfiability, Boolean Modeling and Computation (JSAT)"},{"issue":"2","key":"8_CR4","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/375827.375835","volume":"48","author":"E Ben-Sasson","year":"2001","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. J. ACM 48(2), 149\u2013169 (2001)","journal-title":"J. ACM"},{"key":"8_CR5","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., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"8_CR7","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":"8_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)"},{"issue":"2","key":"8_CR9","doi-asserted-by":"publisher","first-page":"161","DOI":"10.3233\/AIC-140640","volume":"28","author":"M Janota","year":"2015","unstructured":"Janota, M., Lynce, I., Marques-Silva, J.: Algorithms for computing backbones of propositional formulae. AI Commun. 28(2), 161\u2013177 (2015)","journal-title":"AI Commun."},{"key":"8_CR10","unstructured":"Kroening, D., Strichman, O.: Decision procedures - an algorithmic point of view. Theoretical Computer Science. Springer-Verlag, February 2008 (to be published)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"8_CR12","unstructured":"Nadel, A.: Understanding and Improving a Modern SAT Solver. PhD thesis, Tel Aviv University, Tel Aviv, Israel, August 2009"},{"key":"8_CR13","unstructured":"Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Bloem, R., Sharygina, N. (eds.) FMCAD (2010)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Nadel, A., Ryvchin, V., Strichman, O.: Efficient MUS extraction with resolution. In: FMCAD, pp. 197\u2013200. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679410"},{"key":"8_CR15","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":"8_CR16","unstructured":"Shtrichman, O.: Sharing information between instances of a propositional satisfiability (SAT) problem, December 2000. US provisional patent (60\/257,384). Later became patent US2002\/0123867 A1"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/3-540-44798-9_4","volume-title":"Correct Hardware Design and Verification Methods","author":"O Shtrichman","year":"2001","unstructured":"Shtrichman, O.: Pruning techniques for the SAT-based bounded model checking problem. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 58\u201370. Springer, Heidelberg (2001)"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Whittemore, J., Kim, J., Sakallah, K.: Satire: a new incremental satisfiability engine. In: IEEE\/ACM Design Automation Conference (DAC) (2001)","DOI":"10.1145\/378239.379019"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing -- SAT 2015"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24318-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T05:07:24Z","timestamp":1782364044000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-24318-4_8"}},"subtitle":["A New Kind of Incremental Data"],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243177","9783319243184"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24318-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"27 October 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}