Projekt SAT und CSP-Solving
Voraussetzungen
- Programmierkenntnisse
- Interesse an Algorithmen für NP-harte Probleme
- Vordiplom / Bachelor
Themen
- Parallel zur Vorlesung SAT Solving können verschiedene Algorithmen die dort vorgestellt werden implementiert und mit Hilfe des EDACC Systems evaluiert werden.
- Innerhalb des EDACC System werden sogenannte Konfiguratoren eingebungen, die in der Lage sind für eine gegebenen Algorithmus die optimalen Parameter zu finden bezogen auf eine Menge von Zielprobleme die gelöst werden sollen. Für einen Konfiguratot steht eine API zur Verfügung die es ermöglicht schnell Algorithem zu entwicklen und zu testen. Dabei spiele parallele Algorithmen eine sehr große Rolle, da die Ausführungsebene von EDACC bis zu mehreren hunderten von CPU's gleichzeitig bereitstellen kann.
Interessante Links
- Experiment Design and Adminstration for Computer Cluster
- Meldungen rundum das SAT- Problem
- SAT Bibliothek für Java
- Solver und Benchamrks rundum SAT
- Wettbewerbe der SAT-Solver
SAT in Ulm - lokale Seite der Mitarbeiter die sich mit dem SAT-Problem beschäftigen
- Solver und Benchmarks rundum das CSP - Problem
Literatur
- Stochastic Local Search Foundations and Applications - Hoos, Holger H.; Stützle, Thomas
- Handbook of Satisfiability - Biere, A.; Heule, M.; Van Maaren, H.; Walsh, T.;
Die Bücher stehen in der Abteilung zur Verfügung.
Verantwortlich
Termine & Raum
Vorbesprechung am
12.04 Dienstag 16:00-18:00
Raum 531/O27