SAtRes    Offers    Efficient Distributed Clause Vivification

Efficient Distributed Clause Vivification

We deal with the scalable solving 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. Apart from pure CDCL search (conflict driven clause learning), solvers also perform preprocessing and inprocessing routines, where they try to optimize their clause database in specific ways. We recently observed that splitting preprocessing into its own dedicated threads greatly reduces the redundant work being done, gives solvers more time to spend in pure CDCL search, and increases overall performance [1].

We now would like to extend this approach also to inprocessing routines. One prime candidate would be vivification, where solvers try to reduce the size of a given clause by detecting literals that can be safely removed from the clause. This shrinks the clause, increasing its information content. We would like to investigate having solvers not only exchange conflict clauses but also promising vivified clauses. Since multiple solvers often vivified the same clause in the past, it might be beneficial to run vivification also on dedicated threads. The vivification threads could communicate with each other to divide the work in a sensible manner, potentially also in some optimized way to exploit overlaps in clauses. We hope that this technique improves the practical performance of parallel/distributed SAT solving.

The thesis should include a prior literature review on directly relevant topics from SAT research and subsequently offers a design space for own research, especially with respect to the division of work between the vivification threads and sharing of vivification-specific knowledge. 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

[1]: Schreiber, Dominik, Niccolò Rigi-Luperti, and Armin Biere. “Streamlining Distributed SAT Solver Design.” Theory and Applications of Satisfiability Testing (SAT) 23 (2025): 1-23.