DROPS

Artifact

Software

Supplementary material for SAT'25 publication "Streamlining Distributed SAT Solver Design"

Authors: Dominik Schreiber, Niccolò Rigi-Luperti, and Armin Biere

Abstract

Cite as

Dominik Schreiber, Niccolò Rigi-Luperti, Armin Biere. Supplementary material for SAT'25 publication "Streamlining Distributed SAT Solver Design" (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24204,
   title = {{Supplementary material for SAT'25 publication "Streamlining Distributed SAT Solver Design"}}, 
   author = {Schreiber, Dominik and Rigi-Luperti, Niccol\`{o} and Biere, Armin},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:bdecc26fc577de49d3fe853d07e4ba59e3cbe2f8;origin=https://github.com/nrilu/SAT_2025_supplement_63;visit=swh:1:snp:68b6b69da5213d061c6c7608ebac8224b257b641;anchor=swh:1:rev:f8a1918d4fb7a1f8274d91716dd1910c3e703873}{\texttt{swh:1:dir:bdecc26fc577de49d3fe853d07e4ba59e3cbe2f8}} (visited on 2025-08-07)},
   url = {https://github.com/nrilu/SAT_2025_supplement_63},
   doi = {10.4230/artifacts.24204},
}

Document

DOI: 10.4230/LIPIcs.SAT.2025.27

Streamlining Distributed SAT Solver Design

Authors: Dominik Schreiber, Niccolò Rigi-Luperti, and Armin Biere

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract

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.

Cite as

Dominik Schreiber, Niccolò Rigi-Luperti, and Armin Biere. Streamlining Distributed SAT Solver Design. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{schreiber_et_al:LIPIcs.SAT.2025.27,
  author =	{Schreiber, Dominik and Rigi-Luperti, Niccol\`{o} and Biere, Armin},
  title =	{{Streamlining Distributed SAT Solver Design}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{27:1--27:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.27},
  URN =		{urn:nbn:de:0030-drops-237615},
  doi =		{10.4230/LIPIcs.SAT.2025.27},
  annote =	{Keywords: Satisfiability, parallel SAT solving, distributed computing, preprocessing}
}

Search Results

Documents authored by Rigi-Luperti, Niccolò

Supplementary material for SAT'25 publication "Streamlining Distributed SAT Solver Design"

Abstract

Cite as

Streamlining Distributed SAT Solver Design

Abstract

Cite as

Thanks for your feedback!

Could not send message