SAT Solving in der Praxis
- Typ:
- Semester: SS 2018
-
Zeit:
17.04.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
19.04.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
24.04.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
26.04.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
03.05.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
08.05.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
15.05.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
17.05.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
22.05.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
24.05.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
29.05.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
05.06.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
07.06.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
12.06.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
14.06.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
19.06.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
21.06.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
26.06.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
28.06.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
03.07.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
05.07.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
10.07.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
12.07.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
17.07.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
19.07.2018
14:00 - 15:30 wöchentlich
50.34 Raum -120
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. |