Zur Seitennavigation oder mit Tastenkombination für den accesskey-Taste und Taste 1 
Zum Seiteninhalt oder mit Tastenkombination für den accesskey und Taste 2 
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
- 079 B.Sc. Informatik: Wahlpflichtmodul (TIA)
- 079 M.Sc. Informatik (PO-V. 2016): Wahlpflichtmodul (TIA; Vertiefung ALG)
- 105 B.Sc. Mathematik: Wahlpflichtmodul (NF Informatik)
- 105 M.Sc. Mathematik (PO-V. 2010): Wahlpflichtmodul (Angewandte Mathematik; NF Informatik)
- 184 B.Sc. Wirtschaftswissenschaften: Wahlpflichtmodul (IMS: Vertiefungsmodule d. FMI)
- 221 M.Sc. Bioinformatik: Wahlpflichtmodul (Informatik)

Zusammensetzung des Moduls / Lehrformen (V, Ü, S, Praktikum, …)

4 SWS Übung

Inhalte

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

Voraussetzung für die Zulassung zur Modulprüfung

Übungskriterien, die zum Modulbeginn festgelegt und im Vorlesungsverzeichnis kommuniziert werden

Impressum | Datenschutzerklärung