2026-07-24T11:32:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23761 2025-11-12T13:00:18Z ddc:004 open_access

Streamlining Distributed SAT Solver Design Schreiber, Dominik Rigi-Luperti, Niccolò Biere, Armin Satisfiability parallel SAT solving distributed computing preprocessing Distributed clause-sharing SAT solvers have recently been established as powerful automated reasoning tools that can conquer previously infeasible instances. A common design of distributed SAT solvers is to run many off-the-shelf sequential solvers in parallel, employ some diversification (e.g., restart intervals or decision orders), and share conflict clauses among the solver threads. This approach, naïvely, adopts all best practices of sequential solver design for distributed solving, where these practices may be less useful or even actively detrimental. In this work we diagnose such shortcomings in the state-of-the-art system MallobSat and propose first effective mitigations. In particular, we replace the redundant pre- and inprocessing at all threads with single-core preprocessing that runs next to the parallel search, remove LBD values from the clause-sharing operation, and slim down solver diversification to very few lightweight and uniform methods. Experimental evaluations on up to 3072 cores (64 nodes) confirm that our measures improve performance while also drastically simplifying the SAT solving program that is run in parallel. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dominik Schreiber and Niccolò Rigi-Luperti and Armin Biere 2025 Is Part Of LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2025.27 urn:nbn:de:0030-drops-237615 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.27 eng https://creativecommons.org/licenses/by/4.0/legalcode