Modul Theorie effizienter Algorithmen, Informatik (Master) (SPO 8)
Die Studierenden werden befähigt, effiziente Algorithmen in Theorie und Praxis zu entwerfen. Sie können die Korrektheit von diversen graphentheoretischen Problemen mit exakten logischen Schlüssen nachweisen. Sie sind in der Lage, Laufzeiten von Verfahren zu analysieren und passende Analysetechniken einzusetzen. Sie können zudem Modellierungs- und Simulationsverfahren für die computergestützte Auslegung von Prozessabläufen selbstständig implementieren sowie diverse Iterationsverfahren exemplarisch auf modernen Hochleistungsrechnern parallelisieren.
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.
- Tafelanschrieb
- Skript
- Musterlösungen für alle Übungsaufgaben
- T. H. Cormen, C. E. Leiserson, R. L. Rivest, C. Stein: Introduction to Algorithms, 4th edition. MIT Press, 2022.
Die Lehrveranstaltung findet als Vorlesung statt. Begleitende Übungen vertiefen die vermittelten Gebiete.
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. hier:
- 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 vermittelt Studierenden die theoretischen und schwerpunktmäßig praktischen Aspekte des SAT-Solvings. 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 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.