Institut für Theoretische Informatik

1: Lehre.
- 1.1: Vorlesungen.
- 1.2: Projekte.
- 1.3: Seminare.
- 1.4: Proseminare.
- 1.5: Promotionskolleg.
- 1.6: Abschlussarbeiten.
- 1.7: Diplomandenseminar.
- 1.8: Archiv.
  - 1.8.1: WS 2011/2012.
  - 1.8.2: SS 2011.
  - 1.8.3: WS 2010/2011.
  - 1.8.4: SoSe 2010.
  - 1.8.5: WS 2009/2010.
  - 1.8.6: SoSe 2009.
    - 1.8.6.1: Praktika.
    - 1.8.6.2: Seminare.
    - 1.8.6.3: Vorlesungen.
      - 3471216055--.1:7: SAT Solving.
      - 3471191035--.2:7: Datenkompression.
      - 3471187755--.3:7: Kryptologie.
      - 3471180905--.4:7: Kombinatorische Methoden der Informatik.
      - 3471180915--.5:7: Berechenbarkeit und Komplexität.
      - 3471185435--.6:7: Logik.
      - 3471185415--.7:7: Algorithmen der Bioinformatik.
  - 1.8.7: WS 2008/2009.
  - 1.8.8: SoSe 2008.
  - 1.8.9: WS 2007/2008.
2: Forschung.
3: TheorieTag.
4: Mitarbeiter.
5: Adresse.
6: Intern.
7: Impressum.

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.

Dozent

Prof. Dr. Uwe Schöning

Vorlesungszeiten

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

Übungsleiter

keiner

Tutorien

keine