Module / Prüfungen
| Modul |
Prüfungsnummer |
Titel |
VE.Nr. |
Veranstaltungseinheit |
|
|
P-Nr. : 65591
|
Algorithmisches Beweisen LAB: Klausur o. mündl. Prüfung
|
|
65593 |
Algorithmisches Beweisen LAB: Praktikum |
|
FMI-IN3162
|
Mastermodul Algorithmik/Theoretische Informatik II - 6 LP |
|
P-Nr. : 352121
|
Mastermodul Algorithmik/Theoretische Informatik II - 6 LP: mündl. o. schriftl. Prüfung
|
|
352123 |
Mastermodul Algorithmik/Theoretische Informatik II - 6 LP: Vorlesung/Übung/Praktikum |
|
FMI-IN3163
|
Mastermodul Algorithmik/Theoretische Informatik III - 6 LP |
|
P-Nr. : 352131
|
Mastermodul Algorithmik/Theoretische Informatik III - 6 LP: mündl. o. schriftl. Prüfung
|
|
352133 |
Mastermodul Algorithmik/Theoretische Informatik III - 6 LP: Vorlesung/Übung/Praktikum |
|
FMI-IN3161
|
Mastermodul Algorithmik/Theoretische Informatik I - 6 LP |
|
P-Nr. : 352111
|
Mastermodul Algorithmik/Theoretische Informatik I - 6 LP: mündl. o. schriftl. Prüfung
|
|
352113 |
Mastermodul Algorithmik/Theoretische Informatik I - 6 LP: Vorlesung/Übung/Praktikum |
|
FMI-IN3164
|
Mastermodul Algorithmik/Theoretische Informatik IV - 6 LP |
|
P-Nr. : 352141
|
Mastermodul Algorithmik/Theoretische Informatik IV - 6 LP: mündl. o. schriftl. Prüfung
|
|
352143 |
Mastermodul Algorithmik/Theoretische Informatik IV - 6 LP: Vorlesung/Übung/Praktikum |
Inhalt
| Kommentar |
|
| 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
|
| Bemerkung |
Umfang: 4 SWS Praktikum
Leistungspunkte: 4 |
| Voraussetzungen |
Empfohlene bzw. erwartete Vorkenntnisse:
- FMI-IN0001 Algorithmen und Datenstrukturen
- FMI-IN0005 Automaten und Berechenbarkeit
|
| Leistungsnachweis |
Voraussetzung für die Zulassung zur Modulprüfung:
- Übungskriterien, die zum Modulbeginn festgelegt werden
Voraussetzung für die Vergabe von Leistungspunkten (Prüfungsform)
- Klausur oder mündliche Prüfung (Festlegung erfolgt zu Beginn des Moduls)
|
| Lerninhalte |
Inhalt:
Algorithmische Begleitung der Vorlesung Algorithmisches Beweisen;
Prototyp-Implementierungen von Algorithmen zum SAT-Solving:
- Hornformel
- 2-KNF
- Lokale Suche, random walk
- DPLL, CDCL
- QBF Expansion
Experimente mit Solvern
- Testen einfacher/harter Formeln
- Kodierung von Problemen
- Analyse von Formelklassen
- Zufällige Formeln
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
|
| Zielgruppe |
- 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
|
