{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T22:23:56Z","timestamp":1742941436700,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642449727"},{"type":"electronic","value":"9783642449734"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-44973-4_6","type":"book-chapter","created":{"date-parts":[[2013,11,25]],"date-time":"2013-11-25T08:47:05Z","timestamp":1385369225000},"page":"52-58","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Sharing Information in Parallel Search with Search Space Partitioning"],"prefix":"10.1007","author":[{"given":"Davide","family":"Lanti","sequence":"first","affiliation":[]},{"given":"Norbert","family":"Manthey","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,11,26]]},"reference":[{"key":"6_CR1","first-page":"166","volume-title":"IEA\/AIE 2012. LNCS","author":"P Gro\u00dfmann","year":"2012","unstructured":"Gro\u00dfmann, P., H\u00f6lldobler, S., Manthey, N., Nachtigall, K., Opitz, J., Steinke, P.: Solving periodic event scheduling problems with SAT. In: Jiang, H., Ding, W., Ali, M., Wu, X. (eds.) IEA\/AIE 2012. LNCS, vol. 7345, pp. 166\u2013175. Springer, Heidelberg (2012)"},{"issue":"2","key":"6_CR2","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1287\/mnsc.35.2.164","volume":"35","author":"J Carlier","year":"1989","unstructured":"Carlier, J., Pinson, E.: An algorithm for solving the job-shop problem. Manage. Sci. 35(2), 164\u2013176 (1989)","journal-title":"Manage. Sci."},{"key":"6_CR3","volume-title":"Handbook of Constraint Programming (Foundations of Artificial Intelligence)","author":"F Rossi","year":"2006","unstructured":"Rossi, F., Beek, P.V., Walsh, T.: Handbook of Constraint Programming (Foundations of Artificial Intelligence). Elsevier Science Inc, New York (2006)"},{"volume-title":"Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)","key":"6_CR4"},{"issue":"4","key":"6_CR5","first-page":"245","volume":"6","author":"Y Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Manysat: a parallel sat solver. JSAT 6(4), 245\u2013262 (2009)","journal-title":"JSAT"},{"unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Report Series Technical Report 10\/1. Johannes Kepler University, Linz, Austria (2010)","key":"6_CR6"},{"key":"6_CR7","first-page":"502","volume-title":"SAT 2003. LNCS","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)"},{"key":"6_CR8","first-page":"252","volume-title":"CP 2010. LNCS","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)"},{"key":"6_CR9","first-page":"372","volume-title":"LPAR-17. LNCS","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-17. LNCS, vol. 6397, pp. 372\u2013386. Springer, Heidelberg (2010)"},{"key":"6_CR10","first-page":"385","volume-title":"CP 2011. LNCS","author":"AEJ 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. 6876, pp. 385\u2013399. Springer, Heidelberg (2011)"},{"key":"6_CR11","first-page":"46","volume-title":"LION 2011. LNCS","author":"A Arbelaez","year":"2011","unstructured":"Arbelaez, A., Hamadi, Y.: Improving parallel local search for SAT. In: Coello, C.A.C. (ed.) LION 2011. LNCS, vol. 6683, pp. 46\u201360. Springer, Heidelberg (2011)"},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5, 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"5","key":"6_CR13","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques Silva","year":"1999","unstructured":"Marques Silva, J.P., Sakallah, K.A.: Grasp: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"6_CR14","first-page":"343","volume-title":"SAT 2011. LNCS","author":"H Katebi","year":"2011","unstructured":"Katebi, H., Sakallah, K.A., Marques-Silva, J.: Empirical study of the anatomy of modern sat solvers. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 343\u2013356. Springer, Heidelberg (2011)"},{"unstructured":"B\u00f6hm, M., Speckenmeyer, E.: A fast parallel sat-solver - efficient workload balancing, (1994)","key":"6_CR15"},{"issue":"3","key":"6_CR16","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/s10601-012-9121-3","volume":"17","author":"R Martins","year":"2012","unstructured":"Martins, R., Manquinho, V., Lynce, I.: An overview of parallel sat solving. Constraints 17(3), 304\u2013347 (2012)","journal-title":"Constraints"},{"unstructured":"H\u00f6lldobler, S., Manthey, N., Nguyen, V., Stecklina, J., Steinke, P.: A short overview on modern parallel SAT-solvers. In: Wasito, I., et al. (ed.) ICACSIS, pp. 201\u2013206 (2011)","key":"6_CR17"},{"unstructured":"Manthey, N.: Parallel SAT solving - using more cores. In: Pragmatics of SAT(POS\u201911) (2011)","key":"6_CR18"},{"key":"6_CR19","first-page":"200","volume-title":"SAT 2012. LNCS","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)"},{"key":"6_CR20","first-page":"214","volume-title":"SAT 2012. LNCS","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-asserted-by":"crossref","unstructured":"Lanti, D., Manthey, N.: Sharing information in parallel search with search space partitioning. Technical Report 1, Knowledge Representation and Reasoning Group, Technische Universit\u00e4t Dresden, 01062 Dresden, Germany (2013)","key":"6_CR21","DOI":"10.1007\/978-3-642-44973-4_6"},{"key":"6_CR22","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term rewriting and all that","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, New York (1998)"}],"container-title":["Lecture Notes in Computer Science","Learning and Intelligent Optimization"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-44973-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,9]],"date-time":"2023-02-09T21:00:03Z","timestamp":1675976403000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-44973-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642449727","9783642449734"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-44973-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]},"assertion":[{"value":"26 November 2013","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}