Algorithmisches Beweisen LAB
|
Modultitel (deutsch) |
Algorithmisches Beweisen LAB |
|
Modultitel (englisch) |
Proof Complexity and Solving LAB |
|
Modul-Verantwortliche/r |
Olaf Beyersdorff, Joshua Blinkhorn |
|
Voraussetzung für die Zulassung zum Modul |
keine |
|
Art des Moduls (Pflicht-, Wahlpflicht- oder Wahlmodul) |
Wahlpflichtmodul (TIA, ALG) für den M.Sc. Informatik Wahlpflichtmodul für den B.Sc. Informatik Wahlpflichtmodul (Bereich Informatik) für den M.Sc. Bioinformatik Wahlpflichtmodul (Angewandte Mathematik, Vertiefung Algorithmik, Nebenfach Informatik) für den M.Sc. Mathematik Wahlpflichtmodul (Nebenfach Informatik) für den B.Sc. Mathematik Wahlpflichtmodul für den B.Sc. Wirtschaftswissenschaften, Schwerpunkt IMS Wahlpflichtmodul für den B.A. Ergänzungsfach Informatik |
|
Zusammensetzung des Moduls / Lehrformen (V, Ü, S, Praktikum, …) |
4 Praktikum |
|
Leistungspunkte (ECTS credits) |
4 LP |
|
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 |
|
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 |