PSAT
PSAT
Parallel Satisfiability Testing
- Contact Sibylle Möhle
- Authors Steffen Hölldobler, Norbert Manthey
- since 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.
Technical Reports
Refining Unsatisfiable Cores in Incremental SAT Solving
Technical Report, TU Dresden, September 2015
Details Download
An A-Maze-ing SAT Solving Visualization
Technical Report, TU Dresden, April 2015
Details Download
