{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T06:41:13Z","timestamp":1761979273139,"version":"build-2065373602"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642452208"},{"type":"electronic","value":"9783642452215"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45221-5_33","type":"book-chapter","created":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T09:28:23Z","timestamp":1386235703000},"page":"490-502","source":"Crossref","is-referenced-by-count":2,"title":["Partial Backtracking in CDCL Solvers"],"prefix":"10.1007","author":[{"given":"Chuan","family":"Jiang","sequence":"first","affiliation":[]},{"given":"Ting","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"5","key":"33_CR1","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 Transactions on Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Transactions on Computers"},{"key":"33_CR2","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1016\/S1571-0653(04)00322-1","volume":"9","author":"I. Lynce","year":"2001","unstructured":"Lynce, I., Baptista, L., Marques-Silva, J.P.: Stochastic systematic search algorithms for satisfiability. Electronic Notes in Discrete Mathematics\u00a09, 190\u2013204 (2001)","journal-title":"Electronic Notes in Discrete Mathematics"},{"issue":"12","key":"33_CR3","doi-asserted-by":"publisher","first-page":"1604","DOI":"10.1016\/j.dam.2005.10.021","volume":"155","author":"I. Lynce","year":"2007","unstructured":"Lynce, I., Marques-Silva, J.P.: Random backtracking in backtrack search algorithms for satisfiability. Discrete Applied Mathematics\u00a0155(12), 1604\u20131612 (2007)","journal-title":"Discrete Applied Mathematics"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: Proceedings of the 38th Conference on Design Automation, New York, USA, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-72788-0_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"K. Pipatsrisawat","year":"2007","unstructured":"Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 294\u2013299. Springer, Heidelberg (2007)"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning sat solvers. In: Handbook of Satisfiability, pp. 131\u2013154 (2009)","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"33_CR7","doi-asserted-by":"crossref","first-page":"133","DOI":"10.3233\/SAT190082","volume":"7","author":"P. Tak van der","year":"2011","unstructured":"van der Tak, P., Ramos, A., Heule, M.: Reusing the assignment trail in cdcl solvers. Journal on Satisfiability, Boolean Modeling and Computation\u00a07, 133\u2013138 (2011)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"33_CR8","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proceedings of the 2001 IEEE\/ACM International Conference on Computer-Aided Design, pp. 279\u2013285. IEEE Press (2001)"},{"key":"33_CR9","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Minisat 2.2, http:\/\/minisat.se\/"},{"key":"33_CR10","unstructured":"Balint, A., Belov, A., J\u00e4rvisalo, M., Sinz, C.: Sat challenge (2012), http:\/\/baldur.iti.kit.edu\/SAT-Challenge-2012\/index.html"},{"key":"33_CR11","unstructured":"Audemard, G., Simon, L.: Glucose 2.2, https:\/\/www.lri.fr\/~simon\/?page=glucose"}],"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_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T02:08:14Z","timestamp":1746065294000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45221-5_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642452208","9783642452215"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45221-5_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}