DROPS

Artifact

Software

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

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}
}

Search Results

Documents authored by Dörr, Michael

PalRUP-Check

Abstract

Cite as

rubenGoetz/SAT26_experimental_data

Abstract

Cite as

A Natively Parallel Proof Framework for Clause-Sharing SAT Solving

Abstract

Cite as

Thanks for your feedback!

Could not send message