{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:20:55Z","timestamp":1770290455240,"version":"3.49.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319662626","type":"print"},{"value":"9783319662633","type":"electronic"}],"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_15","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T08:05:11Z","timestamp":1502179511000},"page":"233-250","source":"Crossref","is-referenced-by-count":24,"title":["PaInleSS: A Framework for Parallel SAT Solving"],"prefix":"10.1007","author":[{"given":"Ludovic","family":"Le Frioux","sequence":"first","affiliation":[]},{"given":"Souheib","family":"Baarir","sequence":"additional","affiliation":[]},{"given":"Julien","family":"Sopena","sequence":"additional","affiliation":[]},{"given":"Fabrice","family":"Kordon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"key":"15_CR1","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":"15_CR2","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI, vol. 9, pp. 399\u2013404 (2009)"},{"key":"15_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":"15_CR4","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":"15_CR5","unstructured":"Biere, A.: Splatz, lingeling, plingeling, treengeling, yalsat entering the SAT competition 2016. SAT COMPETITION 2016, p. 44 (2016)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). doi: 10.1007\/3-540-49059-0_14"},{"key":"15_CR7","unstructured":"Blochinger, W.: Towards robustness in parallel SAT solving. In: PARCO, pp. 301\u2013308 (2005)"},{"issue":"7","key":"15_CR8","doi-asserted-by":"crossref","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(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"15_CR9","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"15_CR10","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":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61\u201375. Springer, Heidelberg (2005). doi: 10.1007\/11499107_5"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Guo, L., Hamadi, Y., Jabbour, S., Sais, L.: Diversification and intensification in parallel SAT solving. In: International Conference on Principles and Practice of Constraint Programming, pp. 252\u2013265. Springer (2010)","DOI":"10.1007\/978-3-642-15396-9_22"},{"key":"15_CR13","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/978-3-642-21434-9_10","volume-title":"Auton. Search","author":"Y Hamadi","year":"2011","unstructured":"Hamadi, Y., Jabbour, S., Sais, J.: Control-based clause sharing in parallel SAT solving. In: Hamadi, Y., Monfroy, E., Saubion, F. (eds.) Auton. Search, pp. 245\u2013267. Springer, Heidelberg (2011)"},{"key":"15_CR14","doi-asserted-by":"crossref","first-page":"245","DOI":"10.3233\/SAT190070","volume":"6","author":"Y Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. J. Satisfiability Boolean Model. Comput. 6, 245\u2013262 (2009)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"15_CR15","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":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/11814948_39","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"AEJ Hyv\u00e4rinen","year":"2006","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: A distribution method for solving SAT in grids. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 430\u2013435. Springer, Heidelberg (2006). doi: 10.1007\/11814948_39"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-10291-2_25","volume-title":"AI*IA 2009: Emergent Perspectives in Artificial Intelligence","author":"AEJ Hyv\u00e4rinen","year":"2009","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: Partitioning search spaces of a randomized search. In: Serra, R., Cucchiara, R. (eds.) AI*IA 2009. LNCS, vol. 5883, pp. 243\u2013252. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-10291-2_25"},{"key":"15_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":"15_CR19","unstructured":"Kautz, H.A., Selman, B., et al.: Planning as satisfiability. In: ECAI, vol. 92, pp. 359\u2013363 (1992)"},{"key":"15_CR20","unstructured":"Lazaar, N., Hamadi, Y., Jabbour, S., Sebag, M.: Cooperation control in Parallel SAT Solving: a Multi-armed Bandit Approach. Research Report RR-8070, INRIA, September 2012"},{"key":"15_CR21","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":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/11814948_16","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"I Lynce","year":"2006","unstructured":"Lynce, I., Marques-Silva, J.: SAT in bioinformatics: making the case with haplotype inference. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 136\u2013141. Springer, Heidelberg (2006). doi: 10.1007\/11814948_16"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-31612-8_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"N Manthey","year":"2012","unstructured":"Manthey, N.: Coprocessor 2.0 \u2013 a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 436\u2013441. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31612-8_34"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-642-41524-1_18","volume-title":"Applications of Declarative Programming and Knowledge Management","author":"N Manthey","year":"2013","unstructured":"Manthey, N.: Coprocessor \u2013 a standalone SAT preprocessor. In: Tompits, H., Abreu, S., Oetsch, J., P\u00fchrer, J., Seipel, D., Umeda, M., Wolf, A. (eds.) INAP\/WLP -2011. LNCS, vol. 7773, pp. 297\u2013304. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-41524-1_18"},{"issue":"5","key":"15_CR25","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K., et al.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Improving search space splitting for parallel SAT solving. In: IEEE International Conference on Tools with Artificial Intelligence, vol. 1, pp. 336\u2013343. IEEE (2010)","DOI":"10.1109\/ICTAI.2010.56"},{"issue":"1","key":"15_CR27","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1023\/A:1006326723002","volume":"24","author":"F Massacci","year":"2000","unstructured":"Massacci, F., Marraro, L.: Logical cryptanalysis as a SAT problem. J. Autom. Reasoning 24(1), 165\u2013203 (2000)","journal-title":"J. Autom. Reasoning"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, pp. 267\u2013275. ACM (1996)","DOI":"10.1145\/248052.248106"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: 38th annual Design Automation Conference, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"15_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/978-3-642-02777-2_47","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"K Ohmura","year":"2009","unstructured":"Ohmura, K., Ueda, K.: c-sat: A parallel SAT solver for clusters. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 524\u2013537. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02777-2_47"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Schulz, S., Blochinger, W.: Cooperate and compete! a hybrid solving strategy for task-parallel SAT solving on peer-to-peer desktop grids. In: High Performance Computing and Simulation, pp. 314\u2013323. IEEE (2010)","DOI":"10.1109\/HPCS.2010.5547121"},{"key":"15_CR32","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP\u2013a new search algorithm for satisfiability. In: IEEE\/ACM International Conference on Computer-Aided Design, pp. 220\u2013227. IEEE (1997)"},{"key":"15_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-44973-4_25","volume-title":"Learning and Intelligent Optimization","author":"T Sonobe","year":"2013","unstructured":"Sonobe, T., Inaba, M.: Portfolio with block branching for parallel SAT solvers. In: Nicosia, G., Pardalos, P. (eds.) LION 2013. LNCS, vol. 7997, pp. 247\u2013252. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-44973-4_25"},{"issue":"4","key":"15_CR34","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1006\/jsco.1996.0030","volume":"21","author":"H Zhang","year":"1996","unstructured":"Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: a distributed propositional prover and its application to quasigroup problems. J. Symbolic Comput. 21(4), 543\u2013560 (1996)","journal-title":"J. Symbolic Comput."},{"key":"15_CR35","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: IEEE\/ACM International Conference on Computer-Aided Design, pp. 279\u2013285. IEEE Press (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_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,31]],"date-time":"2022-07-31T21:37:08Z","timestamp":1659303428000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}