Search Results

Documents authored by Schreiber, Dominik

Artifact
Software
DOI: 10.4230/artifacts.26960
PalRUP-Check

Authors: Ruben Götz, Michael Dörr, and Dominik Schreiber

Abstract
Cite as

Ruben Götz, Michael Dörr, Dominik Schreiber. PalRUP-Check (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26960,
   title = {{PalRUP-Check}}, 
   author = {G\"{o}tz, Ruben and D\"{o}rr, Michael and Schreiber, Dominik},
   note = {Software, DFG-56540758, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:f9333873d989dbe91482ece76696a5d3d4d5d4c8;origin=https://github.com/rubenGoetz/PalRUP-Check;visit=swh:1:snp:43319bde441703a13c1196b76d10ba9ef0bbfb7d;anchor=swh:1:rev:81d587fff220d21f327a24f6f159349634a49675}{\texttt{swh:1:dir:f9333873d989dbe91482ece76696a5d3d4d5d4c8}} (visited on 2026-07-16)},
   url = {https://github.com/rubenGoetz/PalRUP-Check},
   doi = {10.4230/artifacts.26960},
}
Artifact
Software
DOI: 10.4230/artifacts.26961
Mallob

Authors: Dominik Schreiber, Peter Sanders, Niccolò Rigi-Luperti, and Ruben Götz

Abstract
Cite as

Dominik Schreiber, Peter Sanders, Niccolò Rigi-Luperti, Ruben Götz. Mallob (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26961,
   title = {{Mallob}}, 
   author = {Schreiber, Dominik and Sanders, Peter and Rigi-Luperti, Niccol\`{o} and G\"{o}tz, Ruben},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:63e95b4ba914b33387dbf6e31babbc7b9c3904dc;origin=https://github.com/domschrei/mallob;visit=swh:1:snp:d171a3816db9a89fb89fd452be5b629b191c908c;anchor=swh:1:rev:745c357849212f4dfc33debecac44103a83e5a52}{\texttt{swh:1:dir:63e95b4ba914b33387dbf6e31babbc7b9c3904dc}} (visited on 2026-07-16)},
   url = {https://github.com/domschrei/mallob},
   doi = {10.4230/artifacts.26961},
}
Artifact
Dataset
DOI: 10.4230/artifacts.26962
rubenGoetz/SAT26_experimental_data

Authors: Ruben Götz, Michael Dörr, and Dominik Schreiber

Abstract
Cite as

Ruben Götz, Michael Dörr, Dominik Schreiber. rubenGoetz/SAT26_experimental_data (Dataset). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26962,
   title = {{rubenGoetz/SAT26\underlineexperimental\underlinedata}}, 
   author = {G\"{o}tz, Ruben and D\"{o}rr, Michael and Schreiber, Dominik},
   note = {Dataset, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:18d5082193154a230bf5993b5f6d1b6866a69627;origin=https://github.com/rubenGoetz/SAT26_experimental_data;visit=swh:1:snp:792bfcba7ecf7f18e786862f0df4b49473b14a9e;anchor=swh:1:rev:8c5123eaac03f8fc201b2def536814cba9294082}{\texttt{swh:1:dir:18d5082193154a230bf5993b5f6d1b6866a69627}} (visited on 2026-07-16)},
   url = {https://github.com/rubenGoetz/SAT26_experimental_data},
   doi = {10.4230/artifacts.26962},
}
Document
DOI: 10.4230/LIPIcs.SAT.2026.17
A Natively Parallel Proof Framework for Clause-Sharing SAT Solving

Authors: Ruben Götz, Michael Dörr, and Dominik Schreiber

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract
Unsatisfiability proofs are valuable artifacts in propositional satisfiability (SAT) since they can provide correctness guarantees and thus complete trust in reported results. In powerful parallel and distributed clause-sharing SAT solvers, existing proof technology either funnels all solver threads' relevant reasoning steps into a single proof file, which leads to scalability problems for large setups and long running times, or checks proof information in parallel in real-time, which is fully scalable but leaves no persistent artifact. We suggest an alternative approach to achieve the best of both worlds. Specifically, we consider parallel proof files that are logged and also checked in parallel. To this end, we introduce PalRUP - an LRUP-based proof format and a bottleneck-free, decentralized parallel checking procedure that only uses the (parallel) file system and is composed of a set of small, sequential trusted components. In evaluations on up to 3072 cores, we observe that our approach allows for low-overhead proof logging during solving and substantially outscales prior proof producing approaches in terms of checking performance.
Cite as

Ruben Götz, Michael Dörr, and Dominik Schreiber. A Natively Parallel Proof Framework for Clause-Sharing SAT Solving. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{gotz_et_al:LIPIcs.SAT.2026.17,
  author =	{G\"{o}tz, Ruben and D\"{o}rr, Michael and Schreiber, Dominik},
  title =	{{A Natively Parallel Proof Framework for Clause-Sharing SAT Solving}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{17:1--17:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.17},
  URN =		{urn:nbn:de:0030-drops-263239},
  doi =		{10.4230/LIPIcs.SAT.2026.17},
  annote =	{Keywords: Satisfiability, Proofs, Distributed computing}
}
Document
Tool Paper
DOI: 10.4230/LIPIcs.SAT.2026.40
CaDiCaL 3.0 (Tool Paper)

Authors: Florian Pollitt, Mathias Fleury, Katalin Fazekas, Nils Froleyks, André Schidler, Dominik Schreiber, and Armin Biere

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract
The propositional satisfiability (SAT) solver Kissat supports a relatively narrow feature set in favor of bare-metal performance and targeted improvements to core solving techniques, which helped it dominate the International SAT Competition since 2024. However, many applications rely on advanced SAT solver features such as incremental interaction schemes, finding direct consequences of assumed literals, or expressive proof logging that allows for real-time checking. This system description reports on how we successfully adapted Kissat’s award-winning techniques to the full-featured incremental SAT solver CaDiCaL, including clausal congruence closure, clausal equivalence sweeping, and bounded variable addition. The main challenge was to support efficient linear proof production with hints. We further extended CaDiCaL’s API to extract implied literals under assumptions and applied advanced deterministic scheduling of inprocessing based on the ticks metric for approximating cache line accesses. Experiments confirm the benefits of these efforts.
Cite as

Florian Pollitt, Mathias Fleury, Katalin Fazekas, Nils Froleyks, André Schidler, Dominik Schreiber, and Armin Biere. CaDiCaL 3.0 (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 40:1-40:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{pollitt_et_al:LIPIcs.SAT.2026.40,
  author =	{Pollitt, Florian and Fleury, Mathias and Fazekas, Katalin and Froleyks, Nils and Schidler, Andr\'{e} and Schreiber, Dominik and Biere, Armin},
  title =	{{CaDiCaL 3.0}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{40:1--40:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.40},
  URN =		{urn:nbn:de:0030-drops-263465},
  doi =		{10.4230/LIPIcs.SAT.2026.40},
  annote =	{Keywords: Incremental SAT, CaDiCaL, SAT Solver}
}
Artifact
Software
DOI: 10.4230/artifacts.24204
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}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.25
Trusted Scalable SAT Solving with On-The-Fly LRAT Checking

Authors: Dominik Schreiber

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Recent advances have enabled powerful distributed SAT solvers to emit proofs of unsatisfiability, which renders them as trustworthy as sequential solvers. However, this mode of operation is still lacking behind conventional distributed solving in terms of scalability. We argue that the core limiting factor of such approaches is the requirement of a single, persistent artifact at the end of solving that is then checked independently (and sequentially). As an alternative, we propose a bottleneck-free setup that exploits recent advancements in producing and processing LRAT information to immediately check all solvers' reasoning on-the-fly during solving. In terms of clause sharing, our approach transfers the guarantee of a derived clause’s soundness from the sending to the receiving side via cryptographic signatures. Experiments with up to 2432 cores (32 nodes) indicate that our approach reduces the running time overhead incurred by proof checking by an order of magnitude, down to a median overhead of ≤ 42% over non trusted solving.
Cite as

Dominik Schreiber. Trusted Scalable SAT Solving with On-The-Fly LRAT Checking. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{schreiber:LIPIcs.SAT.2024.25,
  author =	{Schreiber, Dominik},
  title =	{{Trusted Scalable SAT Solving with On-The-Fly LRAT Checking}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.25},
  URN =		{urn:nbn:de:0030-drops-205477},
  doi =		{10.4230/LIPIcs.SAT.2024.25},
  annote =	{Keywords: SAT solving, distributed algorithms, proofs}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact