PSAT
PSAT
Paralleles Lösen des Erfüllbarkeitproblems
- Kontaktperson Sibylle Möhle
- Autoren Norbert Manthey, Steffen Hölldobler
- seit 2015
- finanziert durch DFG
Das Erfüllbarkeitsproblem (SAT) ist ein Standartproblem der Komplexitätsklasse NP mit einer sehr einfachen, aber generischen, Eingabesprache. Durch die Entwicklung der SAT Systeme in den letzten 20 Jahren wird SAT heute genutzt, um Chip-Designs zu verifizieren, um Planungsprobleme wie Car-Sqeuencing zu lösen, um Eigenschaften von Konfigurationen zu verifizieren, oder um Fahrpläne für Bahnnetzwerke zu generieren. Viele weitere diskrete Entscheidungsprobleme können mit Hilfe von SAT gelöst werden. Außerdem können diskrete Optimierungsprobleme auf SAT abgebildet werden und durch mehrfaches Aufrufen des SAT Systems gelöst werden.
In diesem Projekt sollen parallele SAT Systeme entstehen, welche es erlauben auf modernen Mehrkernsystemen, sowie auf Hochleistungsrechnern das Erfüllbarkeitsproblem schneller zu lösen, als es mit sequentiellen Methoden derzeit möglich ist.
Technische Berichte
An A-Maze-ing SAT Solving Visualization
Technical Report, TU Dresden, April 2015
Details Download
Refining Unsatisfiable Cores in Incremental SAT Solving
Technical Report, TU Dresden, September 2015
Details Download
