Stiftungsprofessur für zuverlässige Softwaresysteme in der Automobilindustrie

SAT Solving in der Praxis

  • Typ:
  • Semester: SS 2019
  • Zeit: 23.04.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten


    25.04.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -119
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    30.04.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    02.05.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -119
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    07.05.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    09.05.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -119
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    14.05.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    16.05.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -119
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    21.05.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    23.05.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -119
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    28.05.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    04.06.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    06.06.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -119
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    11.06.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    13.06.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -119
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    18.06.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    25.06.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    27.06.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -119
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    02.07.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    04.07.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -119
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    09.07.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    11.07.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -119
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    16.07.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    18.07.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -119
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    23.07.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -120
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    25.07.2019
    14:00 - 15:30 wöchentlich
    50.34 Raum -119
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten


  • Dozent:
    Prof. Dr. Carsten Sinz
  • SWS: 3
  • LVNr.: 2400085
Lehrinhalt

Das aussagenlogische Erfüllbarkeitsproblem (SAT-Problem) spielt in Theorie und Praxis eine herausragende Rolle. Es ist das erste als NP-vollständig erkannte Problem, und auch heute noch Ausgangspunkt vieler komplexitätstheoretischer Untersuchungen. Darüber hinaus hat sich SAT-Solving inzwischen als eines der wichtigsten grundlegenden Verfahren in der Verifikation von Hard- und Software etabliert und wird zur Lösung schwerer kombinatorischer Probleme auch in der industriellen Praxis verwendet.

Dieses Modul soll Studierenden die theoretischen und praktischen Aspekte des SAT-Solving vermitteln. Behandelt werden:

1. Grundlagen, historische Entwicklung

2. Codierungen, z.B. cardinality constraints

3. Phasenübergänge bei Zufallsproblemen

4. Lokale Suche (GSAT, WalkSAT, …, ProbSAT)

5. Resolution, Davis-Putnam-Algorithmus, DPLL-Algorithmus, Look-Ahead-Algorithmus

6. Effiziente Implementierungen, Datenstrukturen

7. Heuristiken im DPLL-Algorithmus

8. CDCL-Algorithmus, Klausellernen, Implikationsgraphen

9. Restarts und Heuristiken im CDCL-Algorithmus

10. Preprocessing, Inprocessing

11. Generierung von Beweisen und deren Prüfung

12. Paralleles SAT Solving (Guiding Paths, Portfolios, Cube-and-Conquer)

13. Verwandte Probleme: MaxSAT, MUS, #SAT, QBF

14. Fortgeschrittene Anwendungen: Bounded Model Checking, Planen, satisfiability-modulo-theories

Arbeitsbelastung

2 SWS Vorlesung + 1 SWS Übungen

(Vor- und Nachbereitungszeiten: 4h/Woche für Vorlesung plus 2h/Woche für Übungen; Klausurvorbereitung: 15h)

Gesamtaufwand: (2 SWS + 1 SWS + 4 SWS + 2 SWS) x 15h + 15h Klausurvorbereitung = 9x15h + 15h = 150h = 5 ECTS

Ziel

Studierende sind in der Lage, kombinatorische Probleme zu beurteilen, deren Schwere einzuschätzen und mittels Computern zu lösen.

Studierende lernen, wie kombinatorische Probleme mittels SAT Solving effizient gelöst werden können.

Studierende können die praktische Komplexität von Entscheidungs- und Optimierungsproblemen beurteilen, Probleme als SAT-Probleme kodieren und effiziente Lösungsverfahren für kombinatorische Probleme implementieren.