SAT Solving

Klausur

Eine Klausur wird für die SAT Solving Vorlesung nicht angeboten. Prüfungstermine bitte mit Frau Fromm abklären.

Inhalt

Grundlagen

  • Aussagenlogik
  • Normalformen
  • kombinatorische Eigenschaften von (k-)SAT
  • Tseitin-Codierung
  • NP-Vollständigkeit von SAT

Kalkülbasierte Algorithmen

  • Resolution
  • Davis-Putnam (DP)

DPLL-Algorithmen

  • DPLL
  • Heuristiken wie Monien Speckenmeyer
  • Klausellernen

Lokale Suche

  • deterministische lokale Suche mit Überdeckungscodes
  • stochastische lokale Suche (SLS)
  • Heuristiken

Spezialfälle von SAT

  • 2-KNF
  • HORN
  • Mixed-HORN
  • Renamable HORN

SAT Spezialthemen

  • SAT Schwellenwert (phase transition)
  • Lovasz Local Lemma

Literatur:

  • Script
  • Begleit CD zur Vorlesung

 

Übungen

Es gibt weder Tutorien noch Übungen zu dieser Veranstaltung.

Vorlesungszeiten

Montag 14-16 Uhr in o27/122, Donnerstag 12-14 Uhr in o27/122

 

Übungsleiter

keiner

Tutorien

keine