Modul Theorie effizienter Algorithmen, Informatik (Master) (SPO 8)
Das Modul behandelt den Entwurf effizienter Algorithmen in Theorie und Praxis. Die Studierenden erlernen dazu Beweistechniken für graphentheoretische Probleme, um die Korrektheit von Algorithmen mit exakten logischen Schlüssen nachzuweisen. Sie analysieren Laufzeiten von Verfahren und setzen passende Analysetechniken ein. Am Beispiel numerischer Probleme wie z.B. die Interpolation und Approximation mathematischer Modelle konzipieren die Studierenden zudem selbstständig Lösungsverfahren und implementieren diese anschließend. Die Iterationsverfahren werden von den Studierenden für konkrete technische Probleme umgesetzt und exemplarisch zur Nutzung auf modernen Hochleistungsrechnern parallelisiert.
Die Studierenden sind nach Abschluss des Moduls in der Lage, Algorithmen theoretisch zu analysieren und zu bewerten, aber auch Modellierungs- und Simulationsverfahren für die computergestützte Auslegung von Prozessabläufen in der Praxis anzuwenden.
Die Lehrveranstaltung vermittelt grundlegende Algorithmen auf Graphen und zeigt auf, wie man deren Korrektheiten und Zeitkomplexitäten analysiert.
Nach einer kurzen Einführung in die Graphentheorie werden zunächst Durchmusterungsmethoden wie die Breiten- und Tiefensuche vorgestellt. Weitere Algorithmen befassen sich mit der Erkennung von starken Zusammenhangskomponenten, topologischen Sortierungen sowie der Berechnung von kürzesten Wegen. Effiziente Tests auf die Kreisfreiheit von Graphen werden ebenfalls besprochen.
Die Vorlesung befähigt die Teilnehmer, selbstständig weiterführende Algorithmen zu erarbeiten, beweisbar sicher anzuwenden und ihren Nutzen einzuschätzen.
Der Stoff der Vorlesung wird an der Tafel besprochen und ist zusätzlich in einem vorab erhältlichen Skript verfügbar. Skript, Übungsaufgaben und Musterlösungen werden auch online angeboten.
- T. H. Cormen, C. E. Leiserson, R. L. Rivest, C. Stein: Introduction to Algorithms. MIT Press, 2001, ISBN 0-262-03293-7.
Die Lehrveranstaltung findet als Vorlesung statt. Begleitende Übungen vertiefen die vermittelten Gebiete. Musterlösungen werden zur Verfügung gestellt und bei Bedarf auch im Unterricht diskutiert.
SAT-Solving ist eines der wichtigsten allgemeinen Verfahren zur Lösung schwerer (oft NP-vollständiger) kombinatorischer Probleme. Diese treten in der Praxis in einer Vielzahl von Anwendungen auf, z.B.:
- Planungs- und Scheduling-Probleme in Lieferketten
- Konfiguration komplexer, variantenreicher Produkte, z.B. PKWs, LKWs, Flugzeuge
- Prüfung (Verifikation) von Hardware- und Software
- Erstellung von Spielplänen, z.B. in der Bundesliga
Dieses Modul soll Studierenden die theoretischen und schwerpunktmäßig praktischen Aspekte des SAT-Solving vermitteln. Behandelt werden:
- Grundlagen, historische Entwicklung
- Codierungen, z.B. cardinality constraints
- Phasenübergänge bei Zufallsproblemen
- Lokale Suche (GSAT, WalkSAT, ..., ProbSAT)
- Resolution, Davis-Putnam-Algorithmus, DPLL-Algorithmus, Look-Ahead-Algorithmus
- Effiziente Implementierungen, Datenstrukturen
- Heuristiken im DPLL-Algorithmus
- CDCL-Algorithmus, Klausellernen, Implikationsgraphen
- Restarts und Heuristiken im CDCL-Algorithmus
- Preprocessing, Inprocessing
- Generierung von Beweisen und deren Prüfung
- Paralleles SAT Solving (Guiding Paths, Portfolios, Cube-and-Conquer)
- Fortgeschrittene Anwendungen: Bounded Model Checking, Planen, satisfiability-modulo-theories
Auch die Einbindung von industriellen Anwendern (z.B. von Mercedes-Benz) ist vorgesehen.
In dieser Übung werden Verfahren der Vorlesung "Practical SAT Solving" anhand von Fragestellungen aus der Praxis erprobt und SAT-Solver zur Lösung von kombinatorischen Problemen eingesetzt.