{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T10:46:07Z","timestamp":1794480367591,"version":"4.9.1"},"publisher-location":"Cham","reference-count":13,"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_24","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T05:43:21Z","timestamp":1404279801000},"page":"317-332","source":"Crossref","is-referenced-by-count":9,"title":["Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask)"],"prefix":"10.1007","author":[{"given":"Tom\u00e1\u0161","family":"Balyo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andreas","family":"Fr\u00f6hlich","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"24_CR1","series-title":"LNAI","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 (LNAI), vol.\u00a07364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"24_CR2","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O. Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics\u00a096\u201397, 149\u2013176 (1999)","journal-title":"Discrete Applied Mathematics"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-12002-2_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 129\u2013144. Springer, Heidelberg (2010)"},{"issue":"4","key":"24_CR4","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/s10817-011-9239-9","volume":"49","author":"M. J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.H.: Simulating circuit-level simplifications on cnf. Journal of Automated Reasoning\u00a049(4), 583\u2013619 (2012)","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-642-45221-5_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M.J.H. Heule","year":"2013","unstructured":"Heule, M.J.H., Biere, A.: Blocked clause decomposition. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol.\u00a08312, pp. 423\u2013438. Springer, Heidelberg (2013)"},{"key":"24_CR6","unstructured":"Parkes, A.J.: Clustering at the phase transition. In: Proc. of the 14th Nat. Conf. on AI, pp. 340\u2013345. AAAI Press \/ The MIT Press (1997)"},{"key":"24_CR7","unstructured":"Biere, A.: Lingeling, plingeling and treengeling entering the sat competition 2013. In: Balint, A., Belov, M.J.H., Heule, M. (eds.) Proceedings of SAT Competition 2013. Department of Computer Science Series of Publications B, vol.\u00a0B-2013-1, pp. 51\u201352. University of Helsinki (2013)"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.K.: DAG-aware AIG rewriting: A fresh look at combinational logic synthesis. In: Sentovich, E. (ed.) Proceedings of the 43rd Design Automation Conference (DAC 2006), pp. 532\u2013535. ACM (2006)","DOI":"10.1109\/DAC.2006.229287"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R. Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: Abc: An academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 24\u201340. Springer, Heidelberg (2010)"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a021(12) (2002)","DOI":"10.1109\/TCAD.2002.804386"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-31612-8_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A. Balint","year":"2012","unstructured":"Balint, A., Sch\u00f6ning, U.: Choosing probability distributions for stochastic local search and the role of make versus break. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 16\u201329. Springer, Heidelberg (2012)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-642-14186-7_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"A. Balint","year":"2010","unstructured":"Balint, A., Fr\u00f6hlich, A.: Improving stochastic local search for sat with a new probability distribution. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 10\u201315. Springer, Heidelberg (2010)"},{"key":"24_CR13","unstructured":"Li, C., Fan, Y.: Cca2013. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions (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_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T01:39:35Z","timestamp":1558921175000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09284-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319092836","9783319092843"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3_24","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}