{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T21:40:03Z","timestamp":1750801203324,"version":"3.41.0"},"publisher-location":"Cham","reference-count":34,"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_14","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T08:05:11Z","timestamp":1502179511000},"page":"215-232","source":"Crossref","is-referenced-by-count":3,"title":["A Distributed Version of Syrup"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Audemard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Marie","family":"Lagniez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Szczepanski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e9bastien","family":"Tabary","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Aigner, M., Biere, A., Kirsch, C.M., Niemetz, A., Preiner, M.: Analysis of portfolio-style parallel SAT solving on current multi-core architectures. In: Fourth Pragmatics of SAT Workshop, a Workshop of the SAT 2013 Conference, POS 2013, pp. 28\u201340 (2013)","DOI":"10.29007\/73n4"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Amer, A., Lu, H., Balaji, P., Matsuoka, S.: Characterizing MPI and hybrid MPI+threads applications at scale: case study with BFS. In: 15th IEEE\/ACM International Symposium on Cluster, Cloud and Grid Computing, CCGrid 2015, pp. 1075\u20131083 (2015)","DOI":"10.1109\/CCGrid.2015.93"},{"key":"14_CR3","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":"14_CR4","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. 6695, pp. 188\u2013200. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-21581-0_16"},{"key":"14_CR5","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":"14_CR6","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, pp. 399\u2013404 (2009)"},{"key":"14_CR7","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"},{"issue":"1","key":"14_CR8","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1177\/1094342009360206","volume":"24","author":"P Balaji","year":"2010","unstructured":"Balaji, P., Buntinas, D., Goodell, D., Gropp, W., Thakur, R.: Fine-grained multithreading support for hybrid threaded MPI programming. Int. J. High Perform. Comput. Appl. IJHPCA 24(1), 49\u201357 (2010)","journal-title":"Int. J. High Perform. Comput. Appl. IJHPCA"},{"key":"14_CR9","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"},{"key":"14_CR10","unstructured":"Biere, A.: (P)lingeling. http:\/\/fmv.jku.at\/lingeling"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-13217-9_1","volume-title":"Beyond Loop Level Parallelism in OpenMP: Accelerators, Tasking and More","author":"P Carribault","year":"2010","unstructured":"Carribault, P., P\u00e9rache, M., Jourdren, H.: Enabling low-overhead hybrid MPI\/OpenMP parallelism with MPC. In: Sato, M., Hanawa, T., M\u00fcller, M.S., Chapman, B.M., Supinski, B.R. (eds.) IWOMP 2010. LNCS, vol. 6132, pp. 1\u201314. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-13217-9_1"},{"key":"14_CR12","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. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24605-3_37"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Ehlers, T., Nowotka, D., Sieweck, P.: Communication in massively-parallel SAT solving. In: Proceedings of the 26th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2014, pp. 709\u2013716 (2014)","DOI":"10.1109\/ICTAI.2014.111"},{"key":"14_CR14","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"3","volume-title":"Handbook of Satisfiability","author":"J Franco","year":"2009","unstructured":"Franco, J., Martin, J.: A history of satisfiability, Chap.1. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 3\u201374. IOS Press, Amsterdam (2009)"},{"issue":"12","key":"14_CR15","doi-asserted-by":"crossref","first-page":"1549","DOI":"10.1016\/j.dam.2006.10.007","volume":"155","author":"E Goldberg","year":"2007","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: a fast and robust sat-solver. Discrete Appl. Math. 155(12), 1549\u20131561 (2007)","journal-title":"Discrete Appl. Math."},{"key":"14_CR16","unstructured":"Gomes, C.P., Selman, B., Kautz, H.A.: Boosting combinatorial search through randomization. In: Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, AAAI 1998, IAAI 1998, pp. 431\u2013437 (1998)"},{"key":"14_CR17","unstructured":"Grant, R.E., Skjellum, A., Bangalore, P.V.: Lightweight threading with MPI using persistent communications semantics. National Nuclear Security Administration, USA (2015)"},{"issue":"4","key":"14_CR18","first-page":"245","volume":"6","author":"Y Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: ManySat: a parallel SAT solver. J. Satisf. Boolean Model. Comput. JSAT 6(4), 245\u2013262 (2009)","journal-title":"J. Satisf. Boolean Model. Comput. JSAT"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_15"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-319-09284-3_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"B Konev","year":"2014","unstructured":"Konev, B., Lisitsa, A.: A SAT attack on the Erd\u0151s discrepancy conjecture. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 219\u2013226. Springer, Cham (2014). doi: 10.1007\/978-3-319-09284-3_17"},{"issue":"1","key":"14_CR21","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1109\/32.263754","volume":"20","author":"AD Kshemkalyani","year":"1994","unstructured":"Kshemkalyani, A.D., Singhal, M.: Efficient detection and resolution of generalized distributed deadlocks. IEEE Trans. Softw. Eng. TSE 20(1), 43\u201354 (1994)","journal-title":"IEEE Trans. Softw. Eng. TSE"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-642-44973-4_6","volume-title":"Learning and Intelligent Optimization","author":"D Lanti","year":"2013","unstructured":"Lanti, D., Manthey, N.: Sharing information in parallel search with search space partitioning. In: Nicosia, G., Pardalos, P. (eds.) LION 2013. LNCS, vol. 7997, pp. 52\u201358. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-44973-4_6"},{"issue":"6","key":"14_CR23","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1109\/71.862205","volume":"11","author":"S Lodha","year":"2000","unstructured":"Lodha, S., Kshemkalyani, A.D.: A fair distributed mutual exclusion algorithm. IEEE Tran. Parallel Distrib. Syst. (TPDS) 11(6), 537\u2013549 (2000)","journal-title":"IEEE Tran. Parallel Distrib. Syst. (TPDS)"},{"key":"14_CR24","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Proceedings of the 1996 IEEE\/ACM International Conference on Computer-aided Design, ICCAD 1996, pp. 220\u2013227 (1996)"},{"key":"14_CR25","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 Design Automation Conference, DAC 2001, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"14_CR26","unstructured":"MPICH2. http:\/\/www.mcs.anl.gov\/mpi\/mpich2"},{"issue":"3","key":"14_CR27","doi-asserted-by":"crossref","first-page":"344","DOI":"10.1109\/71.80161","volume":"1","author":"S Nishio","year":"1990","unstructured":"Nishio, S., Li, K.F., Manning, E.G.: A resilient mutual exclusion algorithm for computer networks. IEEE Trans. Parallel Distrib. Syst. (TPDS) 1(3), 344\u2013356 (1990)","journal-title":"IEEE Trans. Parallel Distrib. Syst. (TPDS)"},{"key":"14_CR28","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. 4501, pp. 294\u2013299. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-72788-0_28"},{"issue":"1","key":"14_CR29","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1006\/jpdc.1993.1048","volume":"18","author":"M Singhal","year":"1993","unstructured":"Singhal, M.: A taxonomy of distributed mutual exclusion. J. Parallel Distrib. Comput. 18(1), 94\u2013101 (1993)","journal-title":"J. Parallel Distrib. Comput."},{"issue":"2\u20133","key":"14_CR30","first-page":"83","volume":"9","author":"L Smith","year":"2001","unstructured":"Smith, L., Bull, M.: Development of mixed mode MPI\/OpenMP applications. Sci. Program. 9(2\u20133), 83\u201398 (2001)","journal-title":"Sci. Program."},{"key":"14_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-540-75416-9_13","volume-title":"Recent Advances in Parallel Virtual Machine and Message Passing Interface","author":"R Thakur","year":"2007","unstructured":"Thakur, R., Gropp, W.: Test suite for evaluating performance of MPI implementations that support MPI_THREAD_MULTIPLE. In: Cappello, F., Herault, T., Dongarra, J. (eds.) EuroPVM\/MPI 2007. LNCS, vol. 4757, pp. 46\u201355. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-75416-9_13"},{"key":"14_CR32","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"},{"issue":"1","key":"14_CR33","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1109\/TPDS.2013.2297097","volume":"26","author":"W Weigang","year":"2015","unstructured":"Weigang, W., Zhang, J., Luo, A., Cao, J.: Distributed mutual exclusion algorithms for intersection traffic control. IEEE Trans. Parallel Distrib. Syst. (TPDS) 26(1), 65\u201374 (2015)","journal-title":"IEEE Trans. Parallel Distrib. Syst. (TPDS)"},{"key":"14_CR34","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: Proceedings of the International Conference on Computer Aided Design (ICCAD), pp. 279\u2013285 (2001)","DOI":"10.1145\/774572.774637"}],"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_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T20:59:54Z","timestamp":1750798794000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}