SAtRes    Teaching    Information Exchange Beyond Conflict Clauses in Distributed SAT Solving

Information Exchange Beyond Conflict Clauses in Distributed SAT Solving

We deal with the scalable resolution of propositional satisfiability problems (SAT solving), which is a highly practical problem for a wide range of applications (verification, circuit design, cryptanalysis, scheduling, XAI, …). For parallel and distributed SAT solving in high-performance computing environments, e.g., on supercomputers or in clouds, a common technique is to simultaneously run many sequential solvers, which search the space of possible variable assignments in different ways, and let these solvers occasionally exchange selected found conflict clauses. Recent results show that this technique strongly favors solving unsatisfiable instances in particular, while satisfiable instances benefit comparatively little.

Analogous to conflict clauses, we would like to investigate to let the individual solvers not only exchange conflict clauses but also promising (partial) variable assignments, which the solvers find during their search and that already fulfill a large part of the formula. Each solver should then occasionally replace its own current variable assignment with a shared, external variable assignment and thus intensify the search within this subspace. We hope that this technique will improve performance, especially for satisfiable instances.

In line with Praxis der Forschung, the project should include a prior literature review on directly relevant topics from SAT research and subsequently offers a large design space for own research, especially with respect to possible quality and diversity metrics for variable assignments, space-efficient representation of assignments for distributed communication, and the basis for deciding when a solver selects an external assignment (and which one). As part of the hands-on implementation and experimental evaluation, we offer the opportunity to get involved in a world-leading SAT solving system and run the resulting software on a supercomputer. Programming skills in C++ are helpful. There is comprehensive support for the software framework from the supervisor.

Please let us know if you are interested in this project as soon as possible!

Contact: Dominik Schreiber