Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / Bachelor- und Masterarbeiten / Projektbeschreibungen / Untersuchung der Verwendbarkeit von SAT-Solving zur Schulstundenplanung


Inhaltsbereich

Untersuchung der Verwendbarkeit von SAT-Solving zur Schulstundenplanung

Fortgeschrittenenpraktikum


Aufgabenstellung:

Das Erstellen von Schulstundenplänen zu gegebenen Anforderungen ist ein wohlbekanntes NP-vollständiges Problem. In dieser Arbeit soll die Verwendbarkeit von Erfüllbarkeits-Tests für die Aussagenlogik (SAT-Solver) für dieses Problem untersucht werden.
Dazu ist eine Programm zu implementieren, welches aus gegebenen Problemstellungen aussagenlogische Formeln in konjunktiver Normalform (im DIMACS-Datenformat) generiert und diese einem SAT-Solver (als Black Box) zuführt, sowie gegebenenfalls gefundene erfüllende Bewertungen in Stundenpläne zurückübersetzt.
Es sollen dann Beispielprobleme aus Vorarbeiten mit den zur Zeit effizientesten SAT-Solvern, z.B. CHAFF (Princeton University) gelöst und die Performance mit anderen Ansätzen verglichen werden.

Kontakt:

Dr. Jan Johannsen

Artikelaktionen


Funktionsleiste