SAT Solving und Anwendungen
Das aussagenlogische Erfüllbarkeitsproblem (SAT-Problem) spielt in Theorie (Komplexität, NP-Vollständigkeit) und Praxis (Hard- und Software-Verifikation, Konfiguration) eine herausragende Rolle.
Durch große Fortschritte in den letzten Jahren lassen sich heute eine Vielzahl praktischer kombinatorischer Probleme effizient mit SAT-Solvern bearbeiten.
- Grundlagen: Aussagenlogik
- SAT-Solving: Das DPLL-Verfahren
- Moderne Erweiterungen und Verbesserungen
- Implementierungstechniken
- Anwendungsbeispiele
- Übungen zu Theorie und Implementierung; Schreiben eines SAT-Solvers als Mini-Projekt
Art | Vorlesung & Übung |
---|---|
Betreuer | Prof. Dr. Küchlin / Rouven Walter |
Umfang | 2 SWS Vorlesung + 2 SWS Übung / 6 LP |
Termin | Vorlesung: Di, 16 c.t. - 18 Uhr, wöchentlich Übung: Di, 14 c.t. - 16 Uhr, wöchentlich |
Raum | Vorlesung: Sand 14, Seminarraum C118a Übung: Sand 14, Seminarraum C118a / A302 |
Beginn | 18.10.2016 |
Link | Campus / Ilias |