{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:38:45Z","timestamp":1743028725843,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319662626"},{"type":"electronic","value":"9783319662633"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66263-3_16","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T08:05:11Z","timestamp":1502179511000},"page":"251-260","source":"Crossref","is-referenced-by-count":4,"title":["A Propagation Rate Based Splitting Heuristic for Divide-and-Conquer Solvers"],"prefix":"10.1007","author":[{"given":"Saeed","family":"Nejati","sequence":"first","affiliation":[]},{"given":"Zack","family":"Newsham","sequence":"additional","affiliation":[]},{"given":"Joseph","family":"Scott","sequence":"additional","affiliation":[]},{"given":"Jia Hui","family":"Liang","sequence":"additional","affiliation":[]},{"given":"Catherine","family":"Gebotys","sequence":"additional","affiliation":[]},{"given":"Pascal","family":"Poupart","sequence":"additional","affiliation":[]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-31612-8_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"G Audemard","year":"2012","unstructured":"Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.-M., Piette, C.: Revisiting clause exchange in parallel SAT solving. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 200\u2013213. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31612-8_16"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-319-44953-1_3","volume-title":"Principles and Practice of Constraint Programming","author":"G Audemard","year":"2016","unstructured":"Audemard, G., Lagniez, J.-M., Szczepanski, N., Tabary, S.: An adaptive parallel SAT solver. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 30\u201348. Springer, Cham (2016). doi: 10.1007\/978-3-319-44953-1_3"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-319-09284-3_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"G Audemard","year":"2014","unstructured":"Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 197\u2013205. Springer, Cham (2014). doi: 10.1007\/978-3-319-09284-3_15"},{"key":"16_CR4","unstructured":"Audemard, G., Simon, L.: Glucose and syrup in the sat 2016. SAT Compet. pp. 40\u201341 (2016)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-319-24318-4_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"T Balyo","year":"2015","unstructured":"Balyo, T., Sanders, P., Sinz, C.: HordeSat: A massively parallel portfolio SAT solver. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 156\u2013172. Springer, Cham (2015). doi: 10.1007\/978-3-319-24318-4_12"},{"issue":"2","key":"16_CR6","first-page":"65","volume":"2014","author":"A Biere","year":"2014","unstructured":"Biere, A.: Yet another local search solver and lingeling and friends entering the sat competition 2014. SAT Compet. 2014(2), 65 (2014)","journal-title":"SAT Compet."},{"key":"16_CR7","first-page":"44","volume":"2016","author":"A Biere","year":"2016","unstructured":"Biere, A.: Splatz, lingeling, plingeling, treengeling, yalsat entering the sat competition 2016. SAT Compet. 2016, 44 (2016)","journal-title":"SAT Compet."},{"key":"16_CR8","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"16_CR9","volume-title":"Handbook of Satisfiability","author":"A Biere","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS press, Amsterdam (2009)"},{"issue":"2","key":"16_CR10","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1145\/1455518.1455522","volume":"12","author":"C Cadar","year":"2008","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: Automatically generating inputs of death. ACM Trans. Inf. Syst. Secur. 12(2), 10 (2008)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"16_CR11","unstructured":"Chu, G., Stuckey, P.J., Harwood, A.: Pminisat: a parallelization of minisat 2.0. SAT race (2008)"},{"key":"16_CR12","unstructured":"Fujii, H., Fujimoto, N.: Gpu acceleration of bcp procedure for sat algorithms. In: Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA), The Steering Committee of The World Congress in Computer Science, Computer Engineering and Applied Computing (WorldComp), p. 1 (2012)"},{"key":"16_CR13","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780195085914.001.0001","volume-title":"Limits to Parallel Computation: P-Completeness Theory","author":"R Greenlaw","year":"1995","unstructured":"Greenlaw, R., Hoover, H.J., Ruzzo, W.L.: Limits to Parallel Computation: P-Completeness Theory. Oxford University Press on Demand, New York (1995)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-15396-9_22","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2010","author":"L Guo","year":"2010","unstructured":"Guo, L., Hamadi, Y., Jabbour, S., Sais, L.: Diversification and intensification in parallel SAT solving. In: Cohen, D. (ed.) CP 2010. LNCS, vol. 6308, pp. 252\u2013265. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15396-9_22"},{"key":"16_CR15","first-page":"245","volume":"6","author":"Y Hamadi","year":"2008","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Manysat: a parallel SAT solver. J. Satisf. Boolean Model. Comput. 6, 245\u2013262 (2008)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-34188-5_8","volume-title":"Hardware and Software: Verification and Testing","author":"MJH Heule","year":"2012","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50\u201365. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-34188-5_8"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-16242-8_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"AEJ Hyv\u00e4rinen","year":"2010","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: Partitioning SAT instances for distributed solving. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 372\u2013386. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16242-8_27"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-31612-8_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"AEJ Hyv\u00e4rinen","year":"2012","unstructured":"Hyv\u00e4rinen, A.E.J., Manthey, N.: Designing scalable parallel SAT solvers. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 214\u2013227. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31612-8_17"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-319-40970-2_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"JH Liang","year":"2016","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 123\u2013140. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_9"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. In: 1993 Proceedings of the 2nd Israel Symposium on the Theory and Computing Systems, pp. 128\u2013133. IEEE (1993)","DOI":"10.1109\/ISTCS.1993.253477"},{"issue":"3\u20134","key":"16_CR21","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/s13218-015-0406-8","volume":"30","author":"N Manthey","year":"2016","unstructured":"Manthey, N.: Towards next generation sequential and parallel SAT solvers. KI-K\u00fcnstliche Intelligenz 30(3\u20134), 339\u2013342 (2016)","journal-title":"KI-K\u00fcnstliche Intelligenz"},{"key":"16_CR22","unstructured":"Nejati, S., Liang, J.H., Ganesh, V., Gebotys, C., Czarnecki, K.: Adaptive restart and cegar-based solver for inverting cryptographic hash functions. arXiv preprint (2016). arXiv:1608.04720"},{"key":"16_CR23","unstructured":"Nossum, V.: SAT-based preimage attacks on SHA-1. Master\u2019s thesis (2012)"},{"key":"16_CR24","unstructured":"Nossum, V.: Instance generator for encoding preimage, second-preimage, and collision attacks on SHA-1. In: Proceedings of the SAT competition, pp. 119\u2013120 (2013)"},{"key":"16_CR25","first-page":"483","volume":"185","author":"J Rintanen","year":"2009","unstructured":"Rintanen, J.: Planning and SAT. Handb. Satisf. 185, 483\u2013504 (2009)","journal-title":"Handb. Satisf."},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-319-21909-7_21","volume-title":"Parallel Computing Technologies","author":"A Semenov","year":"2015","unstructured":"Semenov, A., Zaikin, O.: Using Monte Carlo method for searching partitionings of hard variants of boolean satisfiability problem. In: Malyshkin, V. (ed.) PaCT 2015. LNCS, vol. 9251, pp. 222\u2013230. Springer, Cham (2015). doi: 10.1007\/978-3-319-21909-7_21"},{"key":"16_CR27","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1016\/j.jpdc.2016.12.014","volume":"106","author":"AA Sohanghpurwala","year":"2016","unstructured":"Sohanghpurwala, A.A., Hassan, M.W., Athanas, P.: Hardware accelerated SAT solvers a survey. J. Parallel Distrib. Comput. 106, 170\u2013184 (2016)","journal-title":"J. Parallel Distrib. Comput."},{"key":"16_CR28","first-page":"28","volume":"2016","author":"M Soos","year":"2016","unstructured":"Soos, M.: The cryptominisat 5 set of solvers at SAT competition 2016. SAT Compet. 2016, 28 (2016)","journal-title":"SAT Compet."},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-642-31612-8_42","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"P Tak","year":"2012","unstructured":"Tak, P., Heule, M.J.H., Biere, A.: Concurrent cube-and-conquer. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 475\u2013476. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31612-8_42"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66263-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,31]],"date-time":"2022-07-31T21:37:09Z","timestamp":1659303429000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}