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 Forschritte 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, M.Sc. Informatik
Umfang	2 SWS Vorlesung + 1 SWS Übung / 4LP
Termin	Vorlesung: Di, 16.c.t - 18 Uhr, wöchentlich Übung: Di, 18 c.t. - 19 Uhr, wöchentlich
Raum	Informatik/Astronomie - Hörsaal A104 (VL + Übung)
Beginn	15.10.2013
Campus Link	Link

Hinweise

Die Übungen zählen zu 30% und die Klausur zählt zu 70% in die Endnote ein
Das 1. Übungsblatt wird am Dienstag, den 22.10.2013, ausgegeben
Die 1. Übungsgruppe findet am Dienstag, den 29.10.2013, statt
Die Vorlesung und Übung findet ab sofort im A104 statt!
Die Vorlesung am 29.10. findet ausnahmsweise im A301 statt; die Übung ist davon nicht betroffen!
Der Abgabetermin für Praxisblatt 4 wurde auf Montag, den 13.1.2014 verschoben.
Am Dienstag, den 7.1.2014 findet deswegen keine Übung statt!
Die Hauptklausur ist korrigiert und die Noten sind am Lehrstuhl ausgehängt.
Für Informationen zur Nachprüfung, siehe Abschnitt unten.

Klausur

Die Klausur findet in der letzten Vorlesung statt:

Dienstag 04. Februar 2014
Hörsaal A301 auf dem Sand
16.00 - 17.00 Uhr

Nachprüfung

Die Nachprüfung findet statt am:

Dienstag, 01. April 2014

Hinweis: Berechtigt an der Nachprüfung teilzunehmen ist, wer die die Hauptklausur nicht bestanden hat, sich abgemeldet hat oder krankheitsbedingt nicht teilnehmen konnte (mit Attest).

Hinweis: Wer an der Nachprüfung teilnehmen möchte, soll sich bitte bis spätestens 28.Feburar 2014 melden bei Rouven Walter (Mail: walterr@informatik.uni-tuebingen.de).

Vorlesungsunterlagen

Hier werden im Laufe der Vorlesung die aktuellen Foliensätze erscheinen. Alte Foliensätze finden Sie weiter unten im Archiv.