184.090 SAT Solving und Erweiterungen
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2019S, VU, 2.0h, 3.0EC

Merkmale

  • Semesterwochenstunden: 2.0
  • ECTS: 3.0
  • Typ: VU Vorlesung mit Übung

Ziele der Lehrveranstaltung

  • Kenntnisse ueber Theorie und Beweisverfahren fuer Aussagenlogik und quantifizierte Aussagenlogik
  • Kenntnisse ueber Anwendungen wie z.B. Planen
  • Praktische Kenntnisse ueber Beweissysteme (z.B. minisat oder depQBF)

Didaktisches Vorgehen

  • Vorlesung mit Frontalvortrag
  • Bearbeitung von einfachen Aufgabenstellungen durch Studierende (z.B. in der Vorlesung präsentierte Beweisskizze fertig machen).
  • Vorbereitung als Hausübung oder durch ca. 10-15 minütige Arbeitsgruppen während der Vorlesung.
  • Kurzpräsentation und Diskussion der Lösungen.
  • Kurzvorstellung von relevanten Aufsätzen inkl. kurzes schriftliches Review.

Inhalt der Lehrveranstaltung

  • Syntax, Semantik, etc. der angegebenen Logiken
  • Beweisverfahren fuer die Logiken insbesonder Quantifizierte Boolesche Formeln
  • Neuere Entwicklungen wie z.B. Beweiser fuer Nichtnormalform, Schaltkreise, Zertifikate und deren Extraktion aus Beweisen etc.
  • Arbeiten mit ausgewaehlten Beweisern
  • Implementierungen (z.B. Präprozessoren)  als weiterfuehrendes Praktikum.
  • Eine detaillierte Präsentation des Inhalts fuer dieses SS erfolgt in der ersten Vorlesungseinheit

Weitere Informationen

ECTS breakdown

  • 18h: 9 lectures a 2h
  • 15h: 3 ex sheets a 5 ex; including preparation of a solution in pdf)
  •  6h: ex presentation
  •  8h: reading a research paper (in teams of 2 students)
  • 12h: preparation of paper presentation
  •   7h: presentation (10 teams, 3 presentations in a 2h slot)
  •   8h:preparation for final exam
  •  1h: final exam

Vorsicht: Daten zu den Pruefungen entstammen dem letzten Studienjahr. Werden in der Vorbesprechung ausgemacht.

Vortragende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Mo.12:00 - 14:0020.05.2019 Besprechungsraum Menger HF0311 (am Institut)SAT Solving und Erweiterungen
Mo.14:00 - 17:0027.05.2019EI 6 Eckert HS SAT Solving und Erweiterungen
Di.10:00 - 12:0004.06.2019Seminarraum FAV 01 A (Seminarraum 183/2) SAT Solving und Erweiterungen
Mi.14:00 - 18:0005.06.2019 Besprechungsraum Menger am Institut (HF0311)SAT Solving und Erweiterungen
Fr.11:00 - 14:0014.06.2019FAV Hörsaal 2 SAT Solving und Erweiterungen
Mo.12:00 - 14:0017.06.2019EI 6 Eckert HS SAT Solving und Erweiterungen

Leistungsnachweis

schriftlich and mündlich

LVA-Anmeldung

Nicht erforderlich

Curricula

Literatur

Aktuelle Literatur wie Artikel aus Fachzeitschriften, dem Handbook of Satisfiability, etc. wird in der Vorlesung bekannt gegeben.

Vorkenntnisse

1) Aussagen- und Praedikatenlogik:

   a) Syntax, Normalformen und Normalformtransformationen,

   b) Semantik, Evaluierung einer gegebenen Formel bzgl. einer
      gegebenen Interpretation, Konzept der logischen Folgerbarkeit
      (entailment) auch unter Theorien, Ueberfuehrung von Validity,
      Entailment, Equivalence und Satisfiablity ineinander,
      Beweisverfahren (Tableau, Sequenzsysteme oder NK anwenden
      koennen)

2) Einfache Beweise fuehren:

   a) Prinzip des Induktionsbeweis (+ einfache Beispiele)

   b) Einfache Beispiele zur Abschaetzung von Laufzeiten und
      Speicherbedarf (Beispiel: Zeige, dass die Zeitkomplexitaet der
      Breitensuche bei fixem Verzweigungsgrad b und Tiefe d in O(b^d)
      liegt. Erwartet wird ein formal korrekter Beweis
      inkl. Erklaerungen wie O-Notation.)

Die Vorkenntnisse entstammen der LVAen Theoretischer Informatik und
Logik (TIL), den formalen Methoden, AlgoDat und einfuehrenden
Mathematikveranstaltungen.  Fuer einen Teil der Logikkenntnisse
koennen u.U. das TIL Skriptum und die Folien von Block Satisfiability (SAT)
unter http://www.logic.at/lvas/fminf/ nuetzlich sein.

Weitere Informationen

Sprache

Englisch