Proseminar "Das Erfüllbarkeitsproblem SAT (2) 5LP" (WS 2012/2013), Vorlesungsnummer: 67260
Viele Probleme in der Hard- und Softwareverifikation können durch aussagenlogische Formeln modelliert werden. Das Verifikationsproblem entspricht dann dem Erfüllbarkeitsproblem (satisfyability problem, SAT) der aussagenlogischen Formeln. Daher sind effiziente Lösungsverfahren für SAT in der Praxis von großer Bedeutung. In diesem Proseminar besprechen wir die Theorie, Algorithmen und Anwendungen von SAT.
Vorbesprechung: 16. Oktober 2012, 16:00 - 17:00 Uhr
Die Vorbesprechung findet in Raum 630, Gebäde E1 5 statt. Alle Themen werden
dabei von uns vorgestellt. Sie erhalten dann die Möglichkeit, sich ein Vortragsthema auszusuchen und mit Ihrem
Betreuer in Kontakt zu treten.
- Einführung in SAT: 7. November 2012, 16:00 Uhr, Raum 401, Gebäude E1 3
Download der Folien
- Probevorträge:
Download der Folien
Dienstag, 4. Dezember 2012 16:00 Uhr
- André Zenner - Boolean Logic
- Nico Herbig - CNF Translation
- Matthias Hennemann - Preprocessing
Mittwoch, 12. Dezember 2012, 16:00 Uhr
- Niklas Brachmann - Resolution
- Frederic Endner-Dühr - Tableaux
- Frank Nedwed - DPLL
Dienstag, 18. Dezember 2012, 16:00 Uhr
- Julian Scherer - DPLL(LA)
- Tobias Frey - CDCL
- Patrick Klitzke - Advanced CDCL: Learned clause reduction
Mittwoch, 9. Januar 2013, 16:00 Uhr
- Florian Sommer - Implementation: Variable Selection Heuristics
- Immanuel Haffner - Implementation: Restart
- Alexander Kampmann - Implementation: Propagation 2-Variable
Dienstag, 15. Januar 2013, 16:00 Uhr
- Kim Hao Josef Nguyen - Bit Vector
- Marc Müller - Bounded Model Checking
- Lukas Löhle - Predicate Abstraction
Mittwoch, 23. Januar 2013, 16:00 Uhr
- Chris Baumann - Complexity
- Govinda Sicheneder - Tempalte-based synthesis
- Thomas Müller - Stålmarck's Method
Alle Probevorträge finden im Raum 401, Gebäude E1 3 statt. Die Teilnehmer sind verpflichtet bei 50 % der Termine anwesend zu sein.
- Vorträge:
29. Januar 2013, 16 - 18 Uhr
- André Zenner - Boolean Logic
- Nico Herbig - CNF Translation
30. Januar 2013, 16 - 18 Uhr
- Matthias Hennemann - Preprocessing
- Niklas Brachmann - Resolution
5. Februar 2013, 16 - 18 Uhr
- Tobias Frey - CDCL
- Patrick Klitzke - Advanced CDCL: Learned clause reduction
6. Februar 2013, 16 - 18 Uhr
- Frederic Endner-Dühr - Tableaux
- Frank Nedwed - DPLL
13. Februar 2013, 10 - 12 Uhr
- Julian Scherer - DPLL(LA)
- Florian Sommer - Implementation: Variable Selection Heuristics
13. Februar 2013, 16 - 18 Uhr
- Immanuel Haffner - Implementation: Restart
- Kim Hao Josef Nguyen - Bit Vector
19. Februar 2013, 10 - 12 Uhr
- Marc Müller - Bounded Model Checking
- Lukas Löhle - Predicate Abstraction
20. Februar 2013, 16 - 18 Uhr
- Chris Baumann - Complexity
- Govinda Sicheneder - Tempalte-based synthesis
Vorläufiger Zeitplan
- Jeder Teilnehmer erhält sein Thema und seinen zuständigen Betreuer bis Ende Oktober per Email
- Einarbeitung in das Thema: ca. 4 - 6 Wochen
- Probevortrag (Die Vorträge finden in 3er/4er Blöcken statt)
- Vorbereitung des endgültigen Vortrages (ca. 2 - 3 Wochen)
- Vortrag (3er/4er Blöcke, je 25 Minuten + 10 Minuten Diskussion)
Kenntnisse in theoretischer Informatik, insbesondere Logik sind nützlich aber keine Zulassungsvoraussetzung. Wir werden
eine Einführung in SAT geben.
Sie müssen englische Fachaufsätze lesen können. Die Vorträge können in deutscher Sprache gehalten
werden, wir begrüssen es jedoch wenn der Vortrag auf englisch gehalten wird.
- Handbook of Satisfiability (Frontiers in Artificial Intelligence and Applications)
A. Biere (Editor), M. Heule (Editor), H. Van Maaren (Editor), T. Walsh (Editor)
IOS Press, February 2009
- Einige Hinweise zum Vortragsstil können Sie hier [deutsch] finden.
- How to give a talk
Bitte melden sie sich auf unserer Registrierungsseite an. Das Proseminar ist auf 10 Teilnehmer beschränkt.
Anmeldeschluss: 16. Oktober 2012
Bitte vergessen sie nicht, sich auch bei
HISPOS anzumelden, da wir die Prüfungsanmeldung nicht
automatisch vornehmen können.
Die Benotung erfolgt aufgrund des mündlichen Vortrags.
TeX4PPT ist ein nützliches, kostenloses Tool zum Erstellen von math. Formeln in Powerpoint.
Sie können folgende Präsentationsvorlagen verwenden, können aber auch gerne ihre eigene erstellen: LaTeX (basierend auf dem 'Seminar'-Package), PowerPoint
