PSAT

From International Center for Computational Logic
Toggle side column

PSAT

Parallel Satisfiability Testing

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

Norbert Manthey
Refining Unsatisfiable Cores in Incremental SAT Solving
Technical Report, TU Dresden, September 2015
Details Download

Norbert Manthey
An A-Maze-ing SAT Solving Visualization
Technical Report, TU Dresden, April 2015
Details Download