Projekt SAT und CSP-Solving

• Programmierkenntnisse
• Interesse an Algorithmen für NP-harte Probleme
• Vordiplom / Bachelor

1. Parallel zur Vorlesung SAT Solving können verschiedene Algorithmen die dort vorgestellt werden implementiert und mit Hilfe des EDACC Systems evaluiert werden.
2. 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.

EDACC - Experiment Design and Adminstration for Computer Cluster

EDACC web frontend

SAT Live! - Meldungen rundum das SAT- Problem

SAT for JAVA - SAT Bibliothek für Java

SAT Library - Solver und Benchamrks rundum SAT

SAT Competition - Wettbewerbe der SAT-Solver

SAT in Ulm - lokale Seite der Mitarbeiter die sich mit dem SAT-Problem beschäftigen

CSP Library - Solver und Benchmarks rundum das CSP - Problem

 

1. Stochastic Local Search Foundations and Applications - Hoos, Holger H.; Stützle, Thomas
2. Handbook of Satisfiability - Biere, A.; Heule, M.; Van Maaren, H.; Walsh, T.;

Die Bücher stehen in der Abteilung zur Verfügung.