Parallel Satisfiability Testing
- Contact Sibylle Möhle
- Authors Norbert Manthey, Steffen Hölldobler
- since January 1, 2015
- funded by DFG
Satisfiability testing is one of the representative problems of the complexity class NP with a simple, but very generic, input language. Due to the significant improvements of the 20 years SAT is used nowadays to verify chip designs, to solve planning problems such as car sequencing, to prove properties of configuration specifications, or to generate schedules for train networks. Many more discrete decision problems can be solved with SAT technology. Furthermore, discrete optimization problems can also be solved by calling a SAT solver multiple times.
In the project a parallel SAT solver should be developed, which can exploit the modern multi-core architecture as well as high performance clusters to solve satisfiability testing more efficient than with the current sequential algorithms.