Offers
Unsatisfiability Cores in Distributed SAT SolvingUnsatisfiability Cores 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, …). One relevant feature of SAT solvers is the ability to produce unsatisfiability cores (UNSAT cores). An UNSAT core, or unsatisfiable subset, is a subset of an unsatisfiable formula’s logical constraints (clauses) that is unsatisfiable in and of itself. For any unsatisfiable formula F, a trivial UNSAT core is F itself. Non-trivial UNSAT cores C ⊂ F, or even minimal ones ("Minimally Unsatisfiable Subsets", MUS), are important for iterative SAT-based procedures that need to know why a certain formula is unsatisfiable, and react accordingly. As of yet, large-scale distributed SAT solvers in high-performance computing environments, e.g., on supercomputers or in clouds, do not support reporting UNSAT cores, which limits their use for certain applications.
The advertised project aims to explore how to generate and report non-trivial UNSAT cores in parallel and distributed SAT solving. As a point of departure, prior work on (small-scale) parallel MUS extraction should be considered and revisited. The main task is to design, analyze, and implement a practical US/MUS approach in the cutting-edge distributed SAT solver MallobSat and to evaluate it in terms of running time overhead and obtained quality. Possible avenues are the use of incremental SAT solving and also the analysis of produced proofs of unsatisfiability (both of which MallobSat supports).
The project can be worked on in the scope of a master’s thesis or a Praxis der Forschung 1-year research project. 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