2026-07-20T05:07:40Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26323 2026-07-16T10:50:12Z ddc:004 open_access

A Natively Parallel Proof Framework for Clause-Sharing SAT Solving Götz, Ruben Dörr, Michael Schreiber, Dominik Satisfiability Proofs Distributed computing 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ruben Götz and Michael Dörr and Dominik Schreiber 2026 Is Part Of LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2026.17 urn:nbn:de:0030-drops-263239 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.17 eng https://creativecommons.org/licenses/by/4.0/legalcode