SAtRes    Offers    Advanced Strategies for Malleable SAT Solving

Advanced Strategies for Malleable SAT Solving

We deal with the scalable resolution of propositional satisfiability problems (SAT solving), which is a highly relevant problem for a wide range of applications (verification, circuit design, cryptanalysis, scheduling, XAI, …). Cutting-edge large-scale distributed SAT solving in high-performance computing environments, e.g., on supercomputers or in clouds, achieves best resource efficiency when combined with specialized scheduling strategies that exploit malleability, i.e., the ability of a parallel task (SAT solving task in this case) to deal with a fluctuating amount of computational resources during its execution. So far, malleable SAT solving works by (a) initializing new SAT solver threads when a task expands onto a new processing element and (b) suspending or terminating existing solver threads when a task shrinks. Since all currently active solver threads periodically exchange learned insights (clause sharing), the progress made by a terminated solver thread is not necessarily entirely lost in terms of global progress. Our recent works have shown that this simple malleability already results in good performance if a task’s computational resources increase monotonically and/or if the considered SAT instance is unsatisfiable. However, satisfiable instances hardly profit from fluctuating resources (i.e., solver threads that leave and later re-join).

The advertised qualification thesis is to explore advanced strategies for efficient malleable SAT solving. This may include sending some “starter pack” information to new solver threads joining the computation, transferring a leaving solver thread’s progress (e.g., promising partial variable assignments) to a residual solver thread, or even serializing entire SAT solver states to disk or over the network in order to preserve and later reuse them. As such, the project includes both algorithmic considerations (also questions of asymptotic complexity and I/O or communication volume) as well as practical engineering. As a 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 modern supercomputer. Previous experience with C++ is strongly recommended.

Contact: Dominik Schreiber