{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T04:42:03Z","timestamp":1777092123977,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642316111","type":"print"},{"value":"9783642316128","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31612-8_16","type":"book-chapter","created":{"date-parts":[[2012,6,18]],"date-time":"2012-06-18T05:14:42Z","timestamp":1339996482000},"page":"200-213","source":"Crossref","is-referenced-by-count":22,"title":["Revisiting Clause Exchange in Parallel SAT Solving"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Audemard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Beno\u00eet","family":"Hoessen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sa\u00efd","family":"Jabbour","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Marie","family":"Lagniez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9dric","family":"Piette","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-21581-0_16","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"G. Audemard","year":"2011","unstructured":"Audemard, G., Lagniez, J.-M., Mazure, B., Sa\u00efs, L.: On Freezing and Reactivating Learnt Clauses. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 188\u2013200. Springer, Heidelberg (2011)"},{"key":"16_CR2","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of IJCAI, pp. 399\u2013404 (2009)"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P. Beame","year":"2004","unstructured":"Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research\u00a022, 319\u2013351 (2004)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"16_CR4","unstructured":"Biere, A.: (p)lingeling, \nhttp:\/\/fmv.jku.at\/lingeling"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Chrabakh, W., Wolski, R.: GrADSAT: A parallel SAT solver for the grid. Technical report, UCSB (2003)","DOI":"10.1145\/1048935.1050188"},{"key":"16_CR6","unstructured":"Chu, G., Stuckey, P.J., Harwood, A.: Pminisat: a parallelization of minisat 2.0. Technical report, SAT Race (2008)"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Darwiche, A., Pipatsrisawat, K.: Complete Algorithms, ch. 3, pp. 99\u2013130. IOS Press (2009)","DOI":"10.3233\/978-1-58603-929-5-99"},{"issue":"4","key":"16_CR8","doi-asserted-by":"publisher","first-page":"127","DOI":"10.3233\/SAT190081","volume":"7","author":"Y. Hamadi","year":"2011","unstructured":"Hamadi, Y., Jabbour, S., Piette, C., Sa\u00efs, L.: Deterministic parallel DPLL. Journal on Satisfiability, Boolean Modeling and Computation\u00a07(4), 127\u2013132 (2011)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"16_CR9","unstructured":"Hamadi, Y., Jabbour, S., Sa\u00efs, L.: Control-based clause sharing in parallel SAT solving. In: Proceedings of IJCAI, pp. 499\u2013504 (2009)"},{"key":"16_CR10","doi-asserted-by":"publisher","first-page":"245","DOI":"10.3233\/SAT190070","volume":"6","author":"Y. Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sa\u00efs, L.: Manysat: a parallel SAT solver. Journal on Satisfiability, Boolean Modeling and Computation\u00a06, 245\u2013262 (2009)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-642-23786-7_30","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"A.E.J. Hyv\u00e4rinen","year":"2011","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: Grid-Based SAT Solving with Iterative Partitioning and Clause Learning. In: Lee, J. (ed.) CP 2011. LNCS, vol.\u00a06876, pp. 385\u2013399. Springer, Heidelberg (2011)"},{"key":"16_CR12","unstructured":"Kottler, S., Kaufmann, M.: SArTagnan - a parallel portfolio SAT solver with lockless physical clause sharing. In: Pragmatics of SAT (2011)"},{"issue":"4","key":"16_CR13","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0020-0190(93)90029-9","volume":"47","author":"Michael Luby","year":"1993","unstructured":"Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. In: Proceedings of ISTCS, pp. 128\u2013133 (1993)","journal-title":"Information Processing Letters"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Sakallah, K.: GRASP - A New Search Algorithm for Satisfiability. In: Proceedings of ICCAD, pp. 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"16_CR15","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":"16_CR16","unstructured":"Roussel, O.: ppfolio, \nhttp:\/\/www.cril.univ-artois.fr\/~roussel\/ppfolio"},{"issue":"4","key":"16_CR17","doi-asserted-by":"publisher","first-page":"203","DOI":"10.3233\/SAT190068","volume":"6","author":"T. Schubert","year":"2009","unstructured":"Schubert, T., Lewis, M., Becker, B.: Pamiraxt: Parallel SAT solving with threads and message passing. Journal on Satisfiability, Boolean Modeling and Computation\u00a06(4), 203\u2013222 (2009)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"16_CR18","unstructured":"Soos, M.: Cryptominisat, \nhttp:\/\/www.msoos.org\/cryptominisat2\/"},{"key":"16_CR19","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: Proceedings of ICCAD, pp. 279\u2013285 (2001)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2014 SAT 2012"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31612-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T04:08:51Z","timestamp":1777090131000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-31612-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642316111","9783642316128"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31612-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}