SAtRes    Teaching    Integrating GPUs in Distributed SAT Solving

Integrating GPUs in Distributed 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, …). Large-scale distributed SAT solvers in high-performance computing environments, e.g., on supercomputers or in clouds, only utilize CPUs as of yet. A recent trend in HPC is that an increasing amount of CPU resources is being replaced with graphical processing units (GPUs) and/or related “accelerator” hardware. While numerical applications (such as Machine Learning) profit tremendously from this modern hardware, exploiting them for combinatorial search applications (such as SAT solving) is significantly more challenging. Some recent works in SAT literature showed that GPUs can support and accelerate SAT solving by performing certain special tasks, such as formula simplification, improving learned conflict clauses, or stochastic local search. However, it is unclear to which degree these improvements will translate to distributed scales and how the achieved acceleration relates to the increase in energy consumption.

The advertised project aims to explore the exploitation of GPUs in distributed SAT solving systems. Using previous work on GPU-accelerated SAT solving, the main task is to integrate selected existing “GPU offloading” into the world-leading distributed SAT solving platform Mallob, investigate its impact relative to the scale of solving in terms of solving performance and energy efficiency, and propose changes and improvements to the setup(s) in order to further increase scalability and/or efficiency.

The project can be worked on in the scope of a master’s thesis or a Praxis der Forschung 1-year research project. In both cases, the project should include a prior literature review on directly relevant topics from SAT research, in particular GPU-accelerated SAT solving, and subsequently offers a large design space for research. 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 GPU programming and C++ are strongly recommended.

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

Contact: Dominik Schreiber