Algorithmisches Beweisen LAB

Modultitel (deutsch)

Algorithmisches Beweisen LAB

Modultitel (englisch)

Proof Complexity and Solving LAB

Modul-Verantwortliche/r

Olaf Beyersdorff

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:

  • 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

Termine

Mo. + Fr., 12:00 – 14:00

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