Thema3449: Unterschied zwischen den Versionen

Aktuelle Version vom 29. November 2016, 22:28 Uhr

Improving SAT Solvers Using State-of-the-Art Techniques

Masterarbeit von Norbert Manthey

Betreuer Steffen Hölldobler
Wissensverarbeitung
15. Dezember 2010 – 15. Dezember 2010
Download

Viele Probleme lassen sich als Erfüllbarkeitsproblem (SAT) kodieren.

Innerhalb der letzten Jahre wurden dafür performante Solver entwickelt. Die Leistung von diesen SAT-Solvern übertrifft in vielen Fällen die Leistung der spezifischen Lösungsprogramme für die jeweiligen Probleme. Dadurch werden viele industrierelevante Anwendungen nach SAT kodiert und mit einem SATSolver gelöst. Dabei wächst die Größe der Probleme, wodurch die Anforderungen an SAT-Solver immer weiter steigen.
Um die Auswirkungen der letzten Entwicklung besser verstehen zu können, sollen in dieser Arbeit die einzelnen Techniken, welche in SAT-Solver Einzug erhielten, vorgestellt und analysiert werden. Durch diese Untersuchengen soll gezeigt werden, welche dieser Techniken zu dem Leistungssprung von SAT-Solvern innerhalb der letzten Jahre geführt haben. Durch die Kombination der besten Techniken soll ein SAT-Solver entstehen, der die Leistung eines state-of-the-art SAT-Solvers hat und auch für das Lösen industrieller Probleme geeignet ist. Die aktuellen Techniken sollen in einem kompontenbasierten SAT-Solver implementiert werden, um die Auswirkungen der einzelnen Veränderungen auf die Leistung des Solvers nachvollziehen zu können.
Schwerpunkte:

Analysieren der aktuellen Techniken in modernen SAT-Solvern
Implementieren der neuen Komponenten in einen SAT-Solver
Empirische Untersuchung der Auswirkungen der einzelnen Komponenten und deren Kombination

@@ Zeile 8: / Zeile 8: @@
 |Forschungsgruppe=Wissensverarbeitung
 |Abschlussarbeitsstatus=Abgeschlossen
-|Abgabe=2010
+|Beginn=2010/12/15
+|Abgabe=2010/12/15
 |Ergebnisse=Diplom manthey.pdf
+|Beschreibung DE=Viele Probleme lassen sich als Erfüllbarkeitsproblem (SAT) kodieren.
+Innerhalb der letzten Jahre wurden dafür performante
+Solver entwickelt. Die Leistung von diesen SAT-Solvern übertrifft
+in vielen Fällen die Leistung der spezifischen Lösungsprogramme
+für die jeweiligen Probleme. Dadurch werden viele industrierelevante
+Anwendungen nach SAT kodiert und mit einem SATSolver
+gelöst. Dabei wächst die Größe der Probleme, wodurch
+die Anforderungen an SAT-Solver immer weiter steigen.<br/>
+Um die Auswirkungen der letzten Entwicklung besser verstehen
+zu können, sollen in dieser Arbeit die einzelnen Techniken, welche
+in SAT-Solver Einzug erhielten, vorgestellt und analysiert werden.
+Durch diese Untersuchengen soll gezeigt werden, welche dieser
+Techniken zu dem Leistungssprung von SAT-Solvern innerhalb
+der letzten Jahre geführt haben. Durch die Kombination der
+besten Techniken soll ein SAT-Solver entstehen, der die Leistung
+eines state-of-the-art SAT-Solvers hat und auch für das Lösen
+industrieller Probleme geeignet ist.
+Die aktuellen Techniken sollen in einem kompontenbasierten
+SAT-Solver implementiert werden, um die Auswirkungen der
+einzelnen Veränderungen auf die Leistung des Solvers nachvollziehen
+zu können.<br/>
+Schwerpunkte:
+<ul>
+<li>Analysieren der aktuellen Techniken in modernen
+SAT-Solvern</li>
+<li>Implementieren der neuen Komponenten in einen
+SAT-Solver</li>
+<li>Empirische Untersuchung der Auswirkungen der einzelnen
+Komponenten und deren Kombination</li>
+</ul>
+|Beschreibung EN=Viele Probleme lassen sich als Erfüllbarkeitsproblem (SAT) kodieren.
+Innerhalb der letzten Jahre wurden dafür performante
+Solver entwickelt. Die Leistung von diesen SAT-Solvern übertrifft
+in vielen Fällen die Leistung der spezifischen Lösungsprogramme
+für die jeweiligen Probleme. Dadurch werden viele industrierelevante
+Anwendungen nach SAT kodiert und mit einem SATSolver
+gelöst. Dabei wächst die Größe der Probleme, wodurch
+die Anforderungen an SAT-Solver immer weiter steigen.<br/>
+Um die Auswirkungen der letzten Entwicklung besser verstehen
+zu können, sollen in dieser Arbeit die einzelnen Techniken, welche
+in SAT-Solver Einzug erhielten, vorgestellt und analysiert werden.
+Durch diese Untersuchengen soll gezeigt werden, welche dieser
+Techniken zu dem Leistungssprung von SAT-Solvern innerhalb
+der letzten Jahre geführt haben. Durch die Kombination der
+besten Techniken soll ein SAT-Solver entstehen, der die Leistung
+eines state-of-the-art SAT-Solvers hat und auch für das Lösen
+industrieller Probleme geeignet ist.
+Die aktuellen Techniken sollen in einem kompontenbasierten
+SAT-Solver implementiert werden, um die Auswirkungen der
+einzelnen Veränderungen auf die Leistung des Solvers nachvollziehen
+zu können.<br/>
+Schwerpunkte:
+<ul>
+<li>Analysieren der aktuellen Techniken in modernen
+SAT-Solvern</li>
+<li>Implementieren der neuen Komponenten in einen
+SAT-Solver</li>
+<li>Empirische Untersuchung der Auswirkungen der einzelnen
+Komponenten und deren Kombination</li>
+</ul>
 }}