SAtRes    Offers    Information Exchange Beyond Clauses in Distributed SAT

Information Exchange Beyond Clauses in Distributed SAT

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.

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.

Contact: Niccolò Rigi-Luperti