{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:15:56Z","timestamp":1784837756570,"version":"3.55.0"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T00:00:00Z","timestamp":1748304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T00:00:00Z","timestamp":1748304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["882500"],"award-info":[{"award-number":["882500"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Science Foundation","award":["CCF-2415773"],"award-info":[{"award-number":["CCF-2415773"]}]},{"name":"Karlsruher Institut f\u00fcr Technologie (KIT)"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Distributed clause-sharing SAT solvers can solve challenging problems hundreds of times faster than sequential SAT solvers by sharing derived information among multiple sequential solvers. Unlike sequential solvers, however, distributed solvers have not been able to produce proofs of unsatisfiability in a scalable manner, which limits their use in critical applications. In this work, we present a method to produce unsatisfiability proofs for distributed SAT solvers by combining the partial proofs produced by each sequential solver into a single, linear proof. We first describe a simple sequential algorithm and then present a fully distributed algorithm for proof composition, which is substantially more scalable and general than prior works. Our empirical evaluation with over 1500 solver threads shows that our distributed approach allows proof composition and checking within around 3<jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\times $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mo>\u00d7<\/mml:mo>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> its own (highly competitive) solving time.<\/jats:p>","DOI":"10.1007\/s10817-025-09725-w","type":"journal-article","created":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T10:40:30Z","timestamp":1748342430000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers"],"prefix":"10.1007","volume":"69","author":[{"given":"Dawn","family":"Michaelson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dominik","family":"Schreiber","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin","family":"Kiesl-Reiter","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,5,27]]},"reference":[{"key":"9725_CR1","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proc. IJCAI, pp. 399\u2013404 (2009). https:\/\/www.ijcai.org\/Proceedings\/09\/Papers\/074.pdf"},{"key":"9725_CR2","doi-asserted-by":"publisher","unstructured":"Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.-M., Piette, C.: Revisiting clause exchange in parallel SAT solving. In: Proc. SAT, pp. 200\u2013213 (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_16","DOI":"10.1007\/978-3-642-31612-8_16"},{"key":"9725_CR3","doi-asserted-by":"publisher","unstructured":"Balyo, T., Sanders, P., Sinz, C.: Hordesat: A massively parallel portfolio SAT solver. In: Proc. SAT, pp. 156\u2013172 (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_12","DOI":"10.1007\/978-3-319-24318-4_12"},{"key":"9725_CR4","unstructured":"Biere, A.: Lingeling, Plingeling and Treengeling entering the SAT competition 2013. In: Proc. SAT Competition, vol. 2013, p. 1 (2013)"},{"key":"9725_CR5","unstructured":"Biere, A.: Yet another local search solver and Lingeling and friends entering the SAT competition 2014. In: Proc. SAT Competition, p. 65 (2014)"},{"key":"9725_CR6","unstructured":"Biere, A.: CNF encodings of complete pairwise combinatorial testing of our SAT solver SATCH. In: Proc. SAT Competition, p. 46 (2021)"},{"key":"9725_CR7","unstructured":"Biere, A., Fleury, M.: Gimsatul, IsaSAT, Kissat entering the SAT competition 2022. In: Proc. SAT Competition, pp. 10\u201311 (2022)"},{"key":"9725_CR8","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020. In: Proc. SAT Competition, p. 50 (2020)"},{"key":"9725_CR9","unstructured":"Biere, A., Fleury, M., Froleyks, N., Heule, M.: The SAT museum. In: Proc. Pragmatics of SAT, pp. 72\u201387 (2023). https:\/\/ceur-ws.org\/Vol-3545\/paper6.pdf"},{"key":"9725_CR10","unstructured":"Biere, A., Fleury, M., Pollitt, F.: CaDiCaL_vivinst, IsaSAT, Gimsatul, Kissat, and TabularaSAT entering the SAT competition 2023. In: Proc. SAT Competition, p. 14 (2023)"},{"issue":"7","key":"9725_CR11","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1145\/362686.362692","volume":"13","author":"BH Bloom","year":"1970","unstructured":"Bloom, B.H.: Space\/time trade-offs in hash coding with allowable errors. Commun. ACM 13(7), 422\u2013426 (1970). https:\/\/doi.org\/10.1145\/362686.362692","journal-title":"Commun. ACM"},{"issue":"3","key":"9725_CR12","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s10817-022-09623-5","volume":"66","author":"J Brakensiek","year":"2022","unstructured":"Brakensiek, J., Heule, M.J.H., Mackey, J., Narvaez, D.E.: The resolution of Keller\u2019s conjecture. J. Autom. Reason. 66(3), 277\u2013300 (2022). https:\/\/doi.org\/10.1007\/s10817-022-09623-5","journal-title":"J. Autom. Reason."},{"key":"9725_CR13","doi-asserted-by":"publisher","unstructured":"Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Proc. SAT, pp. 44\u201357 (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_6","DOI":"10.1007\/978-3-642-14186-7_6"},{"key":"9725_CR14","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19, 7\u201334 (2001). https:\/\/doi.org\/10.1023\/A:1011276507260","journal-title":"Formal Methods Syst. Des."},{"key":"9725_CR15","unstructured":"Cook, B.: Automated Reasoning\u2019s Scientific Frontiers. Amazon Science (2021). https:\/\/www.amazon.science\/blog\/automated-reasonings-scientific-frontiers"},{"key":"9725_CR16","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Hunt, W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: Proc. CADE, 10395, 220\u2013236 (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_14","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"9725_CR17","doi-asserted-by":"publisher","unstructured":"Ehlers, T., Nowotka, D., Sieweck, P.: Communication in massively-parallel SAT solving. In: Proc. ICTAI, pp. 709\u2013716 (2014). https:\/\/doi.org\/10.1109\/ictai.2014.111","DOI":"10.1109\/ictai.2014.111"},{"key":"9725_CR18","unstructured":"Fleury, M., Biere, A.: Scalable proof producing multi-threaded SAT solving with Gimsatul through sharing instead of copying clauses. CoRR arXiv:abs\/2207.13577 (2022)"},{"key":"9725_CR19","doi-asserted-by":"publisher","first-page":"103572","DOI":"10.1016\/j.artint.2021.103572","volume":"301","author":"N Froleyks","year":"2021","unstructured":"Froleyks, N., Heule, M.J.H., Iser, M., J\u00e4rvisalo, M., Suda, M.: SAT competition 2020. Artif. Intell. 301, 103572 (2021). https:\/\/doi.org\/10.1016\/j.artint.2021.103572","journal-title":"Artif. Intell."},{"key":"9725_CR20","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297\u2013308 (1985). https:\/\/doi.org\/10.1016\/0304-3975(85)90144-6","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"9725_CR21","doi-asserted-by":"publisher","first-page":"245","DOI":"10.3233\/sat190070","volume":"6","author":"Y Hamadi","year":"2010","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. JSAT 6(4), 245\u2013262 (2010). https:\/\/doi.org\/10.3233\/sat190070","journal-title":"JSAT"},{"key":"9725_CR22","unstructured":"Heule, M.J.H.: The DRAT format and DRAT-trim checker. CoRR arXiv:abs\/1610.06229 (2016)"},{"key":"9725_CR23","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H.: Schur number five. In: Proc. AAAI, vol. 32 (2018). https:\/\/doi.org\/10.1609\/aaai.v32i1.12209","DOI":"10.1609\/aaai.v32i1.12209"},{"key":"9725_CR24","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H.: Proofs of unsatisfiability. In: Handbook of Satisfiability, pp. 635\u2013668 (2021). https:\/\/doi.org\/10.3233\/faia200987","DOI":"10.3233\/faia200987"},{"key":"9725_CR25","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Haifa Verification Conference, pp. 50\u201365 (2011). https:\/\/doi.org\/10.1007\/978-3-642-34188-5_8","DOI":"10.1007\/978-3-642-34188-5_8"},{"key":"9725_CR26","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Hunt, W., Wetzler, N.: Trimming while checking clausal proofs. In: Proc. FMCAD, pp. 181\u2013188 (2013). https:\/\/doi.org\/10.1109\/fmcad.2013.6679408","DOI":"10.1109\/fmcad.2013.6679408"},{"key":"9725_CR27","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Manthey, N., Philipp, T.: Validating unsatisfiability results of clause sharing parallel SAT solvers. In: Proc. Pragmatics of SAT, pp. 12\u201325 (2014). https:\/\/doi.org\/10.29007\/6vwg","DOI":"10.29007\/6vwg"},{"key":"9725_CR28","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Proc. SAT, pp. 228\u2013245 (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_15","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"9725_CR29","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Hunt, W.A., Kaufmann, M., Wetzler, N.: Efficient, verified checking of propositional proofs. In: Proc. ITP, vol. 10499, pp. 269\u2013284 (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_18","DOI":"10.1007\/978-3-319-66107-0_18"},{"key":"9725_CR30","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1023\/A:1021734202931","volume":"31","author":"M Jeon","year":"2003","unstructured":"Jeon, M., Kim, D.: Parallel merge sort with load balancing. J. Parallel Program. 31, 21\u201333 (2003). https:\/\/doi.org\/10.1023\/A:1021734202931","journal-title":"J. Parallel Program."},{"issue":"3","key":"9725_CR31","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/s10817-019-09525-z","volume":"64","author":"P Lammich","year":"2020","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. J. Autom. Reason. 64(3), 513\u2013532 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09525-z","journal-title":"J. Autom. Reason."},{"key":"9725_CR32","doi-asserted-by":"publisher","unstructured":"Le\u00a0Frioux, L., Baarir, S., Sopena, J., Kordon, F.: PaInleSS: a framework for parallel SAT solving. In: Proc. SAT, pp. 233\u2013250 (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_15","DOI":"10.1007\/978-3-319-66263-3_15"},{"key":"9725_CR33","doi-asserted-by":"publisher","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: Boolean satisfiability in electronic design automation. In: Proc. DAC, pp. 675\u2013680 (2000). https:\/\/doi.org\/10.1145\/337292.337611","DOI":"10.1145\/337292.337611"},{"key":"9725_CR34","doi-asserted-by":"publisher","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: CDCL SAT solving. In: Handbook of Satisfiability, pp. 131\u2013153 (2021). https:\/\/doi.org\/10.3233\/faia200987","DOI":"10.3233\/faia200987"},{"key":"9725_CR35","doi-asserted-by":"publisher","unstructured":"Michaelson, D., Schreiber, D., Heule, M.J.H., Kiesl-Reiter, B., Whalen, M.W.: Unsatisfiability proofs for distributed clause-sharing SAT solvers. In: Proc. TACAS, pp. 348\u2013366 (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_18","DOI":"10.1007\/978-3-031-30823-9_18"},{"key":"9725_CR36","doi-asserted-by":"publisher","unstructured":"Oh, C.: Between SAT and UNSAT: the fundamental difference in CDCL SAT. In: Proc. SAT, pp. 307\u2013323 (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_23","DOI":"10.1007\/978-3-319-24318-4_23"},{"key":"9725_CR37","doi-asserted-by":"publisher","unstructured":"Pollitt, F., Fleury, M., Biere, A.: Faster LRAT checking than solving with CaDiCaL. In: Proc. SAT (2023). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2023.21","DOI":"10.4230\/LIPIcs.SAT.2023.21"},{"key":"9725_CR38","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/351827.384249","volume":"5","author":"P Sanders","year":"2000","unstructured":"Sanders, P.: Fast priority queues for cached memory. JEA 5, 7 (2000). https:\/\/doi.org\/10.1145\/351827.384249","journal-title":"JEA"},{"key":"9725_CR39","doi-asserted-by":"publisher","unstructured":"Sanders, P., Schreiber, D.: Decentralized online scheduling of malleable NP-hard jobs. In: Proc. Euro-Par, pp. 119\u2013135 (2022). https:\/\/doi.org\/10.1007\/978-3-031-12597-3_8","DOI":"10.1007\/978-3-031-12597-3_8"},{"key":"9725_CR40","unstructured":"Schreiber, D.: Mallob in the SAT competition 2022. In: Proc. SAT Competition, pp. 46\u201347 (2022)"},{"key":"9725_CR41","unstructured":"Schreiber, D.: Mallob $$\\{$$32,64,1600$$\\}$$ in the SAT competition 2023. In: Proc. SAT Competition, pp. 46\u201347 (2023)"},{"key":"9725_CR42","doi-asserted-by":"publisher","unstructured":"Schreiber, D.: Scalable SAT solving and its application. PhD thesis, Karlsruhe Institute of Technology (2023). https:\/\/doi.org\/10.5445\/IR\/1000165224","DOI":"10.5445\/IR\/1000165224"},{"key":"9725_CR43","doi-asserted-by":"publisher","unstructured":"Schreiber, D.: Trusted scalable SAT solving with on-the-fly LRAT checking. In: Proc. SAT, pp. 25\u201312519 (2024). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2024.25","DOI":"10.4230\/LIPIcs.SAT.2024.25"},{"key":"9725_CR44","doi-asserted-by":"publisher","unstructured":"Schreiber, D., Sanders, P.: Scalable SAT solving in the cloud. In: Proc. SAT, pp. 518\u2013534 (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_35","DOI":"10.1007\/978-3-030-80223-3_35"},{"key":"9725_CR45","doi-asserted-by":"publisher","first-page":"1437","DOI":"10.1613\/jair.1.15827","volume":"80","author":"D Schreiber","year":"2024","unstructured":"Schreiber, D., Sanders, P.: MallobSat: Scalable SAT solving by clause sharing. J. Artif. Intell. Res. (JAIR) 80, 1437\u20131495 (2024). https:\/\/doi.org\/10.1613\/jair.1.15827","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"9725_CR46","doi-asserted-by":"publisher","unstructured":"Subercaseaux, B., Heule, M.J.H.: The packing chromatic number of the infinite square grid is 15. In: Proc. TACAS, pp. 389\u2013406 (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_20","DOI":"10.1007\/978-3-031-30823-9_20"},{"key":"9725_CR47","doi-asserted-by":"publisher","unstructured":"Tan, Y.K., Heule, M.J.H., Myreen, M.O.: cake_lpr: Verified propagation redundancy checking in CakeML. In: Proc. TACAS, pp. 223\u2013241 (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_12","DOI":"10.1007\/978-3-030-72013-1_12"},{"key":"9725_CR48","unstructured":"Van\u00a0Gelder, A.: Verifying RUP proofs of propositional unsatisfiability. In: ISAIM (2008). http:\/\/isaim2008.unl.edu\/PAPERS\/TechnicalProgram\/ISAIM2008_0008_60a1f9b2fd607a61ec9e0feac3f438f8.pdf"},{"key":"9725_CR49","doi-asserted-by":"publisher","unstructured":"Vizel, Y., Weissenbacher, G., Malik, S.: Boolean satisfiability solvers and their applications in model checking. In: Proc. IEEE, vol. 103, pp. 2021\u20132035 (2015). https:\/\/doi.org\/10.1109\/JPROC.2015.2455034","DOI":"10.1109\/JPROC.2015.2455034"},{"key":"9725_CR50","unstructured":"Zhang, X., Chen, Z., Cai, S.: Parkissat: Random shuffle based and pre-processing extended parallel solvers with clause sharing. In: Proc. SAT Competition, p. 51 (2022)"},{"key":"9725_CR51","unstructured":"Zheng, J., He, K., Chen, Z., Zhou, J., Li, C.-M.: Combining hybrid walking strategy with Kissat MAB, CaDiCaL, and LStech-Maple. In: Proc. SAT Competition, p. 20 (2022)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09725-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09725-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09725-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T09:04:12Z","timestamp":1750669452000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09725-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,27]]},"references-count":51,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["9725"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09725-w","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,27]]},"assertion":[{"value":"30 June 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 April 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 May 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"12"}}