Propositional Proofs as Big Data

• Applicant: Dr. Dominik Schreiber
• Subject Area: Security and Dependability, Operating-, Communication- and Distributed Systems ; Theoretical Computer Science
• Term: since 2025
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 565407588

Propositional satisfiability (SAT) solving is a fundamental tool for a plethora of scientific and industrial applications. In recent years, massively parallel SAT solving approaches have gained traction, offering substantial reductions in solving times and allowing to conquer previously infeasible problems. However, while sequential SAT solvers have long been able to output efficiently checkable proofs of an instance's unsatisfiability, scalable parallel and distributed SAT solvers so far are more limited in this sense: Existing proof-backed parallel approaches either feature distinct bottlenecks or fail to generate persistent proof artifacts. Considering that proofs have become a core part of the theory, practice, and empirical research surrounding SAT, this shortcoming presents a pressing issue and hinders the adoption of distributed SAT solving for mission-critical automated reasoning tasks. Our project aims to bridge this research gap by devising formal, algorithmic, and practical frameworks for proof production and checking that are designed for large-scale computations and, as such, fully scalable. Just like distributed operations in Big Data frameworks (e.g., MapReduce or Apache Spark), we argue that proof data should be produced, stored, and checked in parallel and across many nodes. The notion of distributed proof files can unlock parallel and bottleneck-free construction and checking of proofs because it avoids the intrinsic bottlenecks of prior parallel proof production. First, we design, implement, and evaluate a parallel and distributed framework for producing, processing, and checking proofs in a scalable manner. We aim to produce efficient, accessible, and well-documented software artifacts that have realistic prospects to find widespread adoption. In line with the state of the art in proof checking, the next part our project involves obtaining a formally verified implementation of our parallel and distributed proof checking algorithm. Furthermore, in order to have a long-lasting impact, we need to ensure that our framework is sufficiently powerful and full-featured. To this end, we plan to extend our approach to the most widely used proof logging formats, integrate some of the latest and most powerful proof calculi, and add support for combinations of clause sharing with explicit search space splitting. Lastly, we aim to apply our approach to a selection of significant use cases, including mathematical theorem proving and empirical studies on proof structure. This serves the dual purpose of demonstrating the capabilities of our parallel proof framework while also constructively advancing research in terms of an application. All in all, we expect our proposed project to significantly increase the accessibility and dependability of scalable automated reasoning tools for many mission-critical use cases.

• DFG Programme: Research Grants