{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:15Z","timestamp":1776333375743,"version":"3.51.2"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906527","type":"print"},{"value":"9783031906534","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    In the evolving landscape of SAT solving, leveraging parallel computation has become increasingly significant. The portfolio strategy, combined with clause sharing, has emerged as the leading approach for both local and distributed parallelization on CPUs. Frameworks such as Mallob exemplify the effectiveness of this strategy by providing a straightforward method to deploy portfolio parallel solvers across various computing environments. Similarly, the \n\n\"Image missing\"\n                    \n                    framework specializes in local parallelization, offering diverse strategies for task sharing and parallel execution. This enables the adoption of complex hybrid local parallelization techniques, including portfolio, divide-and-conquer, and cube-and-conquer methods.\n                  <\/jats:p>\n                  <jats:p>\n                    This paper presents \n\n\"Image missing\"\n                    \n                    , a new extension of the \n\n\"Image missing\"\n                    \n                    framework to include the distributed portfolio strategy and clause sharing. Our enhancement aims to broaden \n\n\"Image missing\"\n                    \n                    \u2019s functionality, enabling more effective and comprehensive distributed SAT solving methodologies.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-90653-4_3","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T07:05:24Z","timestamp":1746169524000},"page":"45-64","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["D-Painless: A Framework for Distributed Portfolio SAT Solving"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-6074-9686","authenticated-orcid":false,"given":"Mazigh","family":"Saoudi","sequence":"first","affiliation":[]},{"given":"Souheib","family":"Baarir","sequence":"additional","affiliation":[]},{"given":"Julien","family":"Sopena","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5902-6094","authenticated-orcid":false,"given":"Thibault","family":"Lejemble","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"3_CR1","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI. vol.\u00a09, pp. 399\u2013404 (2009)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Audemard, G., Simon, L.: Glucose in the SAT 2014 competition. SAT COMPETITION 2014 p. 31 (2014)","DOI":"10.1016\/B978-0-12-800348-0.00004-3"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: int. conf. on Theory and Applications of Satisfiability Testing. pp. 197\u2013205. Springer (2014)","DOI":"10.1007\/978-3-319-09284-3_15"},{"key":"3_CR4","unstructured":"Balyo, T., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.): Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Series of Publications B, Department of Computer Science, University of Helsinki, Finland (2023)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Balyo, T., Sanders, P., Sinz, C.: Hordesat: A massively parallel portfolio SAT solver. In: Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT). pp. 156\u2013172. Springer (2015)","DOI":"10.1007\/978-3-319-24318-4_12"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Beyer, D., Kanav, S., Richter, C.: Construction of verifier combinations based on off-the-shelf verifiers. In: Johnsen, E.B., Wimmer, M. (eds.) Fundamental Approaches to Software Engineering. pp. 49\u201370. Springer International Publishing, Cham (2022)","DOI":"10.1007\/978-3-030-99429-7_3"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., van Maaren, H.: Handbook of satisfiability: Second edition. IOS Press, Amsterdam, NY (May 2021)","DOI":"10.3233\/FAIA336"},{"key":"3_CR8","unstructured":"Biere, A.: Splatz, lingeling, plingeling, treengeling, yalsat entering the SAT competition 2016. SAT COMPETITION 2016 p. 44 (2016)"},{"key":"3_CR9","unstructured":"Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2017. In: Balyo, T., Heule, M., J\u00e4rvisalo, M. (eds.) Proc.\u00a0of SAT Competition 2017 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2017-1, pp. 14\u201315. University of Helsinki (2017)"},{"key":"3_CR10","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proc.\u00a0of SAT Competition 2020 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Biere, A., J\u00e4rvisalo, M., Kiesl, B.: Preprocessing in SAT solving. In: Handbook of Satisfiability (2021)","DOI":"10.3233\/FAIA200992"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Bloom, B.H.: Space\/time trade-offs in hash coding with allowable errors. Communications of the ACM 13(7), 422\u2013426 (1970)","DOI":"10.1145\/362686.362692"},{"key":"3_CR13","unstructured":"Chen, Z., Zhang, X., Cai, S., Lu, P.: Cdcl solvers with improved local search cooperation and pre-processing. In: Balyo, T., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2022: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, Department of Computer Science, University of Helsinki, Finland (2022)"},{"key":"3_CR14","unstructured":"Chen, Z., Zhang, X., Cai, S., Lu, P.: Cdcl solvers with improved local search cooperation and pre-processing. In: SAT COMPETITION 2022 Proceedings. pp. 37,38 (2022)"},{"key":"3_CR15","unstructured":"Chen, Z., Zhang, X., Qian, Y., Cai, S.: Prs: A new parallel\/distributed framework for SAT. In: SAT COMPETITION 2023 Proceedings. pp. 39,40 (2023)"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Chrabakh, W., Wolski, R.: Gridsat: A chaff-based distributed SAT solver for the grid. ACM\/IEEE SC 2003 Conference (SC\u201903) pp. 37\u201337 (2003)","DOI":"10.1145\/1048935.1050188"},{"key":"3_CR17","unstructured":"Conference, S.: SAT competition website, https:\/\/satcompetition.github.io\/"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT). pp. 502\u2013518. Springer (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"3_CR19","unstructured":"Frioux, L.L., Baarir, S., Sopena, J., Kordon, F.: Modular and efficient divide-and-conquer SAT solver on top of the painless framework. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems (2019)"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Gabriel, E., Fagg, G.E., Bosilca, G., Angskun, T., Dongarra, J.J., Squyres, J.M., Sahay, V., Kambadur, P., Barrett, B., Lumsdaine, A., Castain, R.H., Daniel, D.J., Graham, R.L., Woodall, T.S.: Open MPI: Goals, concept, and design of a next generation MPI implementation. In: Proceedings, 11th European PVM\/MPI Users\u2019 Group Meeting. pp. 97\u2013104. Budapest, Hungary (2004)","DOI":"10.1007\/978-3-540-30218-6_19"},{"key":"3_CR21","unstructured":"Gailly, J.l., Adler, M.: zlib (1995), https:\/\/www.zlib.net\/"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Manysat: a parallel SAT solver. Journal on Satisfiability, Boolean Modeling and Computation 6, 245\u2013262 (2009)","DOI":"10.3233\/SAT190070"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Heisinger, M., Fleury, M., Biere, A.: Distributed cube and conquer with paracooba. In: SAT. Lecture Notes in Computer Science, vol. 12178, pp. 114\u2013122. Springer (2020)","DOI":"10.1007\/978-3-030-51825-7_9"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Heule, M.J., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: Guiding cdcl SAT solvers by lookaheads. In: Haifa Verification Conference. pp. 50\u201365. Springer (2011)","DOI":"10.1007\/978-3-642-34188-5_8"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Hu, K., Chu, Z.: An efficient circuit-based SAT solver and its application in logic equivalence checking. Microelectronics Journal 142, 106005 (2023)","DOI":"10.1016\/j.mejo.2023.106005"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Kleine\u00a0B\u00fcning, M., Balyo, T., Sinz, C.: Using dimspec for bounded and unbounded software model checking. In: Ait-Ameur, Y., Qin, S. (eds.) Formal Methods and Software Engineering. pp. 19\u201335. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-32409-4_2"},{"key":"3_CR27","unstructured":"Kreinovich, V., Nguyen, H.T., Ouncharoen, R.: How to estimate forecasting quality: A system-motivated derivation of symmetric mean absolute percentage error (smape) and other similar characteristics (2014)"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Le\u00a0Frioux, L., Baarir, S., Sopena, J., Kordon, F.: Painless: a framework for parallel SAT solving. In: Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT). pp. 233\u2013250. Springer (2017)","DOI":"10.1007\/978-3-319-66263-3_15"},{"key":"3_CR29","unstructured":"Liang, J.H., Oh, C., Ganesh, V., Czarnecki, K., Poupart, P.: Maplecomsps lrb vsids, and maplecomsps chb vsids. In: Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions. pp. 20\u201321. Department of Computer Science, University of Helsinki, Finland (2017)"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Massacci, F., Marraro, L.: Logical cryptanalysis as a SAT problem. Journal of Automated Reasoning 24, 165\u2013203 (2000)","DOI":"10.1023\/A:1006326723002"},{"key":"3_CR31","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). pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"3_CR32","unstructured":"Qian, Y., Chen, Z., Zhang, X., Cai, S.: Prs-distributed in the SAT competition 2024. In: Proceedings of SAT Competition 2024: Solver and Benchmark Descriptions. Department of Computer Science Report Series B, Department of Computer Science, University of Helsinki, Finland (2024)"},{"key":"3_CR33","unstructured":"Ryan, L.: Efficient algorithms for clause-learning SAT solvers. Ph.D. thesis, Theses (School of Computing Science)\/Simon Fraser University (2004)"},{"key":"3_CR34","unstructured":"Sami\u00a0Cherif, M., Habet, D., Terrioux, C.: Un bandit manchot pour combiner CHB et VSIDS. In: Actes des 16\u00e8mes Journ\u00e9es Francophones de Programmation par Contraintes (JFPC). Nice, France (Jun 2021)"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Schreiber, D.: Lilotane: A lifted SAT-based approach to hierarchical planning. J. Artif. Int. Res. 70, 11171181 (may 2021)","DOI":"10.1613\/jair.1.12520"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"Schreiber, D., Sanders, P.: Scalable SAT solving in the cloud. In: Li, C.M., Many\u00e0, F. (eds.) Theory and Applications of Satisfiability Testing \u2013 SAT 2021. pp. 518\u2013534. Springer International Publishing, Cham (2021)","DOI":"10.1007\/978-3-030-80223-3_35"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Schreiber, D., Sanders, P.: MallobSat: Scalable SAT solving by clause sharing. Journal of Artificial Intelligence Research (JAIR) (2024), presented at Pragmatics of SAT (PoS) 2024","DOI":"10.1613\/jair.1.15827"},{"key":"3_CR38","unstructured":"Silva, J.M., Sakallah, K.A.: Grasp-a new search algorithm for satisfiability. In: Proceedings of International Conference on Computer Aided Design. pp. 220\u2013227. IEEE (1996)"},{"key":"3_CR39","unstructured":"Vallade, V., Baarir, S., Sopena, J.: New concurrent painless solvers based on kissat-mab: P-kissat and p-kissat-str. In: SAT COMPETITION 2023 Proceedings. pp. 42,43 (2023)"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Vallade, V., Le\u00a0Frioux, L., Baarir, S., Sopena, J., Kordon, F.: On the usefulness of clause strengthening in parallel SAT solving. In: Proceedings of the 12th NASA Formal Methods Symposium (NFM). Springer (2020)","DOI":"10.1007\/978-3-030-55754-6_13"},{"key":"3_CR41","unstructured":"Vallade, V., Le\u00a0Frioux, L., Oanea, R., Baarir, S., Sopena, J., Kordon, F., Nejati, S., Ganesh, V.: New concurrent and distributed painless solvers: P-mcomsps, p-mcomsps-com,p-mcomsps-mpi, and p-mcomsps-com-mpi. In: Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions. p.\u00a040. Department of Computer Science, University of Helsinki, Finland (2021)"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: a distributed propositional prover and its application to quasigroup problems. Journal of Symbolic Computation 21(4), 543\u2013560 (1996)","DOI":"10.1006\/jsco.1996.0030"},{"key":"3_CR43","doi-asserted-by":"crossref","unstructured":"Zhang, H., Stickel, M.: Implementing the davis\u2013putnam method. Journal of Automated Reasoning 24(1-2), 277\u2013296 (2000)","DOI":"10.1023\/A:1006351428454"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90653-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:36:39Z","timestamp":1764401799000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90653-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906527","9783031906534"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90653-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}