Research
[ARA] Resource-Efficient Flexible SAT Solving for HPC and Cloud Environments[ARA] Resource-Efficient Flexible SAT Solving for HPC and Cloud Environments
Dominik Schreiber’s proposal Resource-Efficient Flexible SAT Solving for HPC and Cloud Environments was recognized with a 2026 Amazon Research Award. This award entails a gift of cash funding (80k USD) and AWS credits (40k) for our research.
Project duration: N/A (Fall 2025 call, approved Spring 2026)
Funding source: Amazon
Principal Investigator: Dominik Schreiber
Collaboration partners: –
Our proposed project aims to advance automated reasoning in distributed environments such as Clouds and High‐Performance Computing by significantly reducing the startup / provisioning overheads, response times, and resource spending of distributed SAT solving. Specifically, we intend to enhance flexible scheduling protocols for scalable incremental SAT solving by effective progress saving measures. This may involve writing the state of SAT solver threads to disk to resume or migrate them later, as well as caching important shared conflict clauses and using them to warm‐start late joining solver threads in challenging computations. We also aim to reconcile these advances with the scalable checking of proofs of unsatisfiability.