PSAT

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
Toggle side column

PSAT

Paralleles Lösen des Erfüllbarkeitproblems

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

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