Automation of Logic
Deutsch

SAT: Propositionale Erfüllbarkeit und Mehr

Dozenten

Inhalt

Viele Probleme der Hard- und Softwareverifikation sowie der Wissensrepräsentation können durch aussagenlogische Formeln modelliert werden. Die Lösung des Ursprungsproblems 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.

Themen

  1. Syntax und Semantik
  2. Wahrheitstabellen und Tableau
  3. Normalform I: Grundlagen
  4. Normalform II: Weiterführende Techniken
  5. Resolution
  6. Superposition
  7. DPLL
  8. CDCL
  9. Implementierung CDCL
  10. Superposition und CDCL
  11. Komplexität
  12. CDCL Erweiterung: Optimierung
  13. Anwendungen

Termine

Mittwoch, 20.04.2016, 10 - 12 Uhr:

  • Einführung in Propositionale Logik
  • Organisatorisches
  • Verteilung der Themen

Donnerstag, 21.04.2016, 15:00 Uhr:

  • Vorträge halten
  • Feedback geben

Mittwoch, 18.05.2016, 11:15 Uhr:

  • Probevorträge: Heller, Kulesha

Mittwoch, 08.06.2016, 10:15 Uhr:

  • Probevorträge: Brauner, Gehl
  • Vortrag: Resolution (Kulesha)
  • Vortrag: CDCL (Heller)

Mittwoch, 15.06.2016, 10:30 Uhr:

  • Vortrag: Superposition (Gehl)
  • Vortrag: Superposition und CDCL (Brauner)

Alle Termine finden in Gebäude E1 5, Raum 630 statt.

Voraussetzungen

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üßen es jedoch wenn der Vortrag auf Englisch gehalten wird.

Literatur

Die benötigte Literatur wird zur Verfügung gestellt.

Benotung

Die Benotung erfolgt aufgrund des mündlichen Vortrags und einer kurzen schriftlichen Ausarbeitung (max. 2 Seiten).

Anmeldung

Bitte melden Sie sich auf unserer Registrierungsseite an. Das Proseminar ist auf 13 Teilnehmer beschränkt.

Anmeldeschluss: 19. April 2016

Bitte vergessen Sie nicht, sich auch bei HISPOS anzumelden, da wir die Prüfungsanmeldung nicht automatisch vornehmen können.

Verschiedenes

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