{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T15:20:21Z","timestamp":1774365621979,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642452208","type":"print"},{"value":"9783642452215","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45221-5_29","type":"book-chapter","created":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T09:28:23Z","timestamp":1386235703000},"page":"423-438","source":"Crossref","is-referenced-by-count":7,"title":["Blocked Clause Decomposition"],"prefix":"10.1007","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Krohm, F., Kuchlmann, A., Mets, A.: The use of random simulation in formal verification. In: Proceedings of the 1996 IEEE International Conference on Computer Design: VLSI in Computers and Processors, ICCD 1996, pp. 371\u2013376 (1996)","DOI":"10.1109\/ICCD.1996.563581"},{"key":"29_CR2","unstructured":"Kuehlmann, A.: Dynamic transition relation simplification for bounded property checking. In: ICCAD, pp. 50\u201357 (2004)"},{"issue":"4","key":"29_CR3","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":"29_CR4","unstructured":"Parkes, A.J.: Clustering at the phase transition. In: Proceedings of AAAI 1997, pp. 340\u2013345. AAAI Press (1997)"},{"key":"29_CR5","first-page":"1179","volume-title":"Proceedings of IJCAI 2003","author":"W. Zhang","year":"2003","unstructured":"Zhang, W., Rangan, A., Looks, M.: Backbone guided local search for maximum satisfiability. In: Proceedings of IJCAI 2003, pp. 1179\u20131184. Morgan Kaufmann Publishers Inc., San Francisco (2003)"},{"key":"29_CR6","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1613\/jair.711","volume":"12","author":"J. Singer","year":"2000","unstructured":"Singer, J., Gent, I.P., Smaill, A.: Backbone fragility and the local search cost peak. Journal of Artificial Intelligence Research\u00a012, 235\u2013270 (2000)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-38171-3_6","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"M.J.H. Heule","year":"2013","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Revisiting hyper binary resolution. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol.\u00a07874, pp. 77\u201393. Springer, Heidelberg (2013)"},{"key":"29_CR8","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96-97","author":"O. Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics\u00a096-97, 149\u2013176 (1999)","journal-title":"Discrete Applied Mathematics"},{"key":"29_CR9","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":"1","key":"29_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"M. Liffiton","year":"2008","unstructured":"Liffiton, M., Sakallah, K.: Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning\u00a040(1), 1\u201333 (2008)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"29_CR11","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 Commun.\u00a025(2), 97\u2013116 (2012)","journal-title":"AI Commun."},{"key":"29_CR12","unstructured":"Junker, U.: Quickxplain: Preferred explanations and relaxations for over-constrained problems. In: AAAI, pp. 167\u2013172 (2004)"},{"key":"29_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-34188-5_9","volume-title":"Hardware and Software: Verification and Testing","author":"Z. Khasidashvili","year":"2012","unstructured":"Khasidashvili, Z., Nadel, A.: Implicative simultaneous satisfiability and applications. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol.\u00a07261, pp. 66\u201379. Springer, Heidelberg (2012)"},{"key":"29_CR14","unstructured":"Codish, M., Fekete, Y., Metodi, A.: Compiling finite domain constraints to SAT with BEE. In: POS (2013)"},{"key":"29_CR15","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1613\/jair.3809","volume":"46","author":"A. Metodi","year":"2013","unstructured":"Metodi, A., Codish, M., Stuckey, P.J.: Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems. JAIR\u00a046, 303\u2013341 (2013)","journal-title":"JAIR"},{"key":"29_CR16","unstructured":"Janota, M., Lynce, I., Marques-Silva, J.: Experimental analysis of backbone computation algorithms. In: International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, RCRA (2012)"},{"issue":"7","key":"29_CR17","doi-asserted-by":"publisher","first-page":"814","DOI":"10.1109\/43.851997","volume":"19","author":"C.A.J. Eijk van","year":"2000","unstructured":"van Eijk, C.A.J.: Sequential equivalence checking based on structural similarities. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a019(7), 814\u2013819 (2000)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.E.: An n log n algorithm for minimizing states in a finite automaton. Technical report, Stanford, CA, USA (1971)","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"29_CR19","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.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"29_CR20","unstructured":"Biere, A.: Lingeling, Plingeling and Treengeling entering the SAT competition 2013. In: Proceedings of SAT Competition 2013 (2013)"},{"key":"29_CR21","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)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-45221-5_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T02:08:13Z","timestamp":1746065293000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45221-5_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642452208","9783642452215"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45221-5_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}