Name des Moduls | [65590] Algorithmisches Beweisen LAB | Bezeichnung des Moduls | FMI-IN0159 |
Studiengang | [079] - Informatik | ECTS Punkte | 4 |
Arbeitsaufwand für Selbststudium | 60 | Häufigkeit des Angebotes (Modulturnus) | jedes 2. Semester (jährlich) |
Arbeitsaufwand in Präsenzstunden | 60 | Dauer des Moduls | 1 |
Arbeitsaufwand Summe (Workload) | 120 | ||
Modul-Verantwortliche/r | Prof. Dr. Olaf Beyersdorff |
Voraussetzung für die Vergabe von Leistungspunkten (Prüfungsform) | Klausur oder mündliche Prüfung (Festlegung erfolgt zu Beginn des Moduls) |
Empfohlene Literatur | Uwe Schöning, Jacobo Toran: Das Erfüllbarkeitsproblem SAT, Lehmanns 2012 Stasys Jukna: Boolean Function Complexity, Springer 2012 Handbook of Satisfiability, IOS Pres, 2009 |
Voraussetzung für die Zulassung zum Modul | keine |
Empfohlene bzw. erwartete Vorkenntnisse | FMI-IN0001 Algorithmen und Datenstrukturen FMI-IN0005 Automaten und Berechenbarkeit |
Art des Moduls (Pflicht-, Wahlpflicht- oder Wahlmodul) | - 079 B.A. Informatik: Wahlpflichtmodul |
Zusammensetzung des Moduls / Lehrformen (V, Ü, S, Praktikum, …) | 4 SWS Übung |
Inhalte | Algorithmische Begleitung der Vorlesung Algorithmisches Beweisen; Prototyp-Implementierungen von Algorithmen zum SAT-Solving:
Experimente mit Solvern
|
Lern- und Qualifikationsziele | Vertiefte Kenntnisse in Theoretischer Informatik, Logik und der algorithmischen Lösung von Erfüllbarkeitsproblemen Befähigung zur beweistheoretischen Einordnung konkreter Formelklassen Grundverständnis und Befähigung zur Implementierung moderner SAT-Algorithmen Kenntnisse zum Einsatz moderner SAT- und QBF-Solver Einsichten in Chancen und Grenzen moderner SAT-Solver |
Voraussetzung für die Zulassung zur Modulprüfung | Übungskriterien, die zum Modulbeginn festgelegt und im Vorlesungsverzeichnis kommuniziert werden |