Research
Amazon Research Award 2024Amazon Research Award 2024
The proposal From Mavericks to Teamplayers: Fostering Solver Cooperation in Distributed SAT Solving was awarded with a 2024 Amazon Research Award, with Prof. Armin Biere (University of Freiburg) as Principal Investigator, Dominik Schreiber (SAtRes) as associated personnel and (de facto) Co-PI, and Prof. Peter Sanders (Algorithm Engineering, ITI, KIT) as cooperation partner.
The project aims to advance automated reasoning in distributed environments such as Clouds and High-Performance Computing. Current distributed solvers for propositional satisfiability (SAT) feature sequential solvers as mostly independent modules with the only cooperation among them being the exchange of learned conflict clauses. We believe that enhancing the cooperation among solver threads by carefully co-developing the sequential, parallel, and distributed level will result in considerable advances in terms of resource efficiency and speedups. Specifically, we intend to explore:
(a) the combination of hand-crafted shared-memory solvers with distributed clause exchange;
(b) information exchange beyond conflict clauses;
(c) performing selected inprocessing tasks cooperatively.
We also aim to reconcile these advancements with the scalable production of proofs of unsatisfiability.