Algorithmisches Beweisen - Einzelansicht

Uwe Schöning, Jacobo Toran: Das Erfüllbarkeitsproblem SAT, Lehmanns 2012

Jan Krajicek: Bounded Arithmetic, Propositional Logic, and Complexity Theory, Cambridge University Press, 1995

Stasys Jukna: Boolean Function Complexity, Springer 2012

Empfohlene bzw. erwartete Vorkenntnisse:

• FMI-IN0001 Algorithmen und Datenstrukturen
• FMI-IN0005 Automaten und Berechenbarkeit

Voraussetzung für die Zulassung zur Modulprüfung: Übungskriterien, die zum Modulbeginn festgelegt werden

Klausur oder mündliche Prüfung (Festlegung erfolgt zu Beginn des Moduls)

Inhalt:

Einführung in die Beweiskomplexität und algorithmische Aspekte von SAT mit den Themen:

• Wichtige Beweissysteme
• Harte Formeln für Resolution
• Spieltechniken für untere Schranken
• Algorithmen für Spezialfälle (Hornformeln, 2-SAT)
• DPLL und CDCL Algorithmen
• Zusammenhang zwischen Beweissystemen und SAT-Solvern
• Geometrische und algebraische Beweissysteme
• Frege-Kalküle
• Quantifizierte Boolesche Formeln
• Beweissysteme für modale Logik
• Lokale Suchalgorithmen

Lern- und Qualifikationsziele:

• Vertiefte Kenntnisse in Theoretischer Informatik, Logik und der algorithmischen Lösung von Erfüllbarkeitsproblemen.
• Befähigung zur beweistheoretischen Einordnung konkreter Formelklassen
• Kenntnisse über Techniken zum Nachweis unterer Schranken
• Einsichten in Chancen und Grenzen moderner SAT-Solver

• 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