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.

2023S, VU, 2.0h, 3.0EC

Merkmale

  • Semesterwochenstunden: 2.0
  • ECTS: 3.0
  • Typ: VU Vorlesung mit Übung
  • Format der Abhaltung: Hybrid

Lernergebnisse

Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage...

  •     understand and compare many automated reasoning techniques
  •     understand, use and modify advanced data structures and algorithms of modern SAT solvers
  •     select and use relevant techniques and methods to design SAT-based solving algorithms for new problems

Inhalt der Lehrveranstaltung

Topics covered:

  • SAT solving:
    • Algorithms and advanced data structures
    • Formula simplifications in SAT solvers
    • Proofs produced by SAT solvers
  • Satisfiability modulo Theories:
    • Basics of DPLL(T) algorithm, concept of theory solvers
    • Congruence closure algorithm for theory of equality with uninterpreted functions
  • Other extensions of the satisfiability problem:
    • Maximum Satisfiability
    • Quantified Boolean Formulas
  • Practical work with solvers of the presented problems

A more detailed presentation of the content of the summer term will be presented in the first lecture.

Methoden

  • Vorlesung
  • Unterstützende Q+A sessions
  • Praktisches Arbeiten mit Solvern

Prüfungsmodus

Mündlich

Weitere Informationen

Erste Vorlesung (Vorbesprechung): TBA

ECTS breakdown

  • 20h: 9 lectures a 2h + Q+A sessions for the reading + implemenation part
  • 38h: reading a research paper (in teams of 2 students) + presenttation
  •         or implementing a new technique
  • 16h:preparation for final exam
  •  1h: final exam

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

       
 

Es ist geplant, dass die  Einheiten in Präsenz abgehalten werden. Wir behalten uns aber vor, wenn es die Situation erfordern sollte, auf Distance Learning umzustellen. Im Distance Learning würden die Einheiten im gleichen Modus via ZOOM Meetings abgewickelt.

Bei etwaigen Distance Learning ist folgendes Equipment ausreichend: geeigneter Arbeitsplatz, stabile Internetverbindung, Notebook mit integrierter Kamera & Headset (oder vergleichbarer Setup)

Vortragende Personen

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Di.16:00 - 19:0009.05.2023 - 06.06.2023Seminarraum FAV 01 C (Seminarraum 188/2) SAT Solving und Erweiterungen
Di.16:00 - 19:0027.06.2023Seminarraum FAV 01 C (Seminarraum 188/2) SAT Solving und Erweiterungen
SAT Solving und Erweiterungen - Einzeltermine
TagDatumZeitOrtBeschreibung
Di.09.05.202316:00 - 19:00Seminarraum FAV 01 C (Seminarraum 188/2) SAT Solving und Erweiterungen
Di.16.05.202316:00 - 19:00Seminarraum FAV 01 C (Seminarraum 188/2) SAT Solving und Erweiterungen
Di.23.05.202316:00 - 19:00Seminarraum FAV 01 C (Seminarraum 188/2) SAT Solving und Erweiterungen
Di.06.06.202316:00 - 19:00Seminarraum FAV 01 C (Seminarraum 188/2) SAT Solving und Erweiterungen
Di.27.06.202316:00 - 19:00Seminarraum FAV 01 C (Seminarraum 188/2) SAT Solving und Erweiterungen

Leistungsnachweis

Wahlweise Vortrag oder Implementierung einer Technik  plus mündliche Prüfung

 

LVA-Anmeldung

Von Bis Abmeldung bis
23.04.2023 17:00 14.05.2023 20:00

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