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
|
