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.

2024S, VU, 2.0h, 3.0EC
TUWEL

LVA-Bewertung

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
    • Incremental Reasoning
  • Extensions of the satisfiability problem:
    • Maximum Satisfiability
    • Quantified Boolean Formulas
    • Satisfiability modulo Theories
  • Practical work with solvers of the presented problems

The content and organisation of the course will be discussed in more details during an initial meeting (5th March, 18:00, Seminarraum FAV 01 A)
where we will fix the format of the lecture and decide on which day and in which timeslot it will take place.

If you cannot attend this initial meeting, but you would like to participate, please send an email to katalin.fazekas@tuwien.ac.at.

Methoden

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

Prüfungsmodus

Mündlich

Weitere Informationen

Erste Vorlesung (Vorbesprechung): 5th March, 18:00,  Seminarraum FAV 01 A

ECTS breakdown

  • 22h: 10 lectures a 2h + Q+A sessions for the reading + implemenation part
  • 15h: 3 ex sheets; (including preparation of a solution in pdf)
  • 3h: ex presentation
  • 20h: reading a research paper or implementing a technique +
            preparing presentation
  • 6h: paper/project presentation
  • 8h:preparation for final exam
  •  1h: final exam

 Attention: The dates for the exams are from last year. They will be discussed in the first lecture "Vorbesprechung".


The course is planned to be in-person. However, if circumstances require, it will be changed to Distance Learning. In Distance Learning the lectures will be provided via ZOOM meeting.

 

Vortragende Personen

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Di.18:00 - 20:0005.03.2024Seminarraum FAV 01 A (Seminarraum 183/2) Vorbesprechung
Fr.12:00 - 14:0015.03.2024 - 24.05.2024Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fr.13:00 - 15:0019.04.2024Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fr.13:00 - 15:0007.06.2024 - 14.06.2024Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fr.13:00 - 15:0021.06.2024Seminarraum FAV EG B (Seminarraum von Neumann) Lecture
SAT Solving und Erweiterungen - Einzeltermine
TagDatumZeitOrtBeschreibung
Di.05.03.202418:00 - 20:00Seminarraum FAV 01 A (Seminarraum 183/2) Vorbesprechung
Fr.15.03.202412:00 - 14:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fr.22.03.202412:00 - 14:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fr.12.04.202412:00 - 14:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fr.19.04.202413:00 - 15:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fr.03.05.202412:00 - 14:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fr.17.05.202412:00 - 14:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fr.24.05.202412:00 - 14:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fr.07.06.202413:00 - 15:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fr.14.06.202413:00 - 15:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fr.21.06.202413:00 - 15:00Seminarraum FAV EG B (Seminarraum von Neumann) Lecture

Leistungsnachweis

Mündliche Prüfung

 

LVA-Anmeldung

Von Bis Abmeldung bis
08.02.2024 15:00 08.04.2024 23:00

Curricula

StudienkennzahlVerbindlichkeitSemesterAnm.Bed.Info
066 504 Masterstudium Embedded Systems Keine Angabe
066 931 Logic and Computation Gebundenes Wahlfach
066 937 Software Engineering & Internet Computing Gebundenes Wahlfach
066 938 Technische Informatik Gebundenes Wahlfach
881 Informatik Gebundenes Wahlfach

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