PSAT: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Norbert Manthey (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
Norbert Manthey (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| Zeile 5: | Zeile 5: | ||
|Beschreibung DE=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. | |Beschreibung DE=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 | 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. | ||
|Beschreibung EN=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. | |Beschreibung EN=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. | ||
| Zeile 14: | Zeile 14: | ||
|Finanziert von=DFG | |Finanziert von=DFG | ||
|Projektstatus=aktiv | |Projektstatus=aktiv | ||
|Person=Norbert Manthey, Steffen Hölldobler, | |Person=Norbert Manthey, Steffen Hölldobler, | ||
|Forschungsgruppe=Wissensverarbeitung | |Forschungsgruppe=Wissensverarbeitung | ||
}} | }} | ||
Version vom 11. Juni 2015, 09:57 Uhr
PSAT
Paralleles Lösen des Erfüllbarkeitproblems
- Kontaktperson Norbert Manthey
- 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
Norbert Manthey
An A-Maze-ing SAT Solving Visualization
Technical Report, TU Dresden, April 2015
Details Download
Norbert Manthey
Refining Unsatisfiable Cores in Incremental SAT Solving
Technical Report, TU Dresden, September 2015
Details Download
