Grundlagen der Künstlichen Intelligenz V
Constraint-Programmierung
Dieser Kurs ist Teil der Kursreihe „Grundlagen der Künstlichen Intelligenz“, die eine Vielzahl von Algorithmen und Methoden behandelt, die in der KI von zentraler Bedeutung und von großer praktischer Relevanz sind.
Übersicht
Der Kurs „Grundlagen der Künstlichen Intelligenz V“ führt in die Grundlagen der Constraint-Programmierung ein. Der Kurs behandelt Constraint-Satisfaction- und Optimierungsprobleme sowie fortgeschrittene Algorithmen, die zu deren Lösung eingesetzt werden. Er liefert relevante Definitionen für das Constraint-Reasoning, stellt Techniken vor, die in CP-, SAT- und CP-SAT-Solvern verwendet werden, und diskutiert die Modellierung solcher Probleme in der Constraint-Modelliersprache MiniZinc.
Insbesondere besprechen wir, wie die Techniken der Constraint Programming (CP)-Solver und der Satisfiability (SAT)-Solver in CP-SAT-Solvern kombiniert werden, um die Vorteile beider Ansätze zu vereinen. CP-SAT-Solver sind Stand der Technik und können auch extrem komplexe Probleme sehr schnell lösen. Wie Probleme so modelliert werden können, dass diese Algorithmen sie effizient lösen können, wird ebenfalls am Beispiel der Modelliersprache MiniZinc vorgestellt.
Der Kurs nutzt einige der theoretischen Grundlagen, die im Kurs „Logik und Erfüllbarkeit“ dieser Kursreihe behandelt wurden.
Die fundierte theoretische Behandlung der Definitionen und Algorithmen wird durch zahlreiche Beispiele ergänzt.
Der Kurs basiert auf dem Lehrbuch von Stuart Russell und Peter Norvig: Introduction to Artificial Intelligence, 3. Auflage 2012 oder 4. Auflage 2020. Die 3. Auflage ist auch auf Deutsch erhältlich: Stuart Russell und Peter Norvig: Künstliche Intelligenz – Ein Moderner Ansatz, 3. aktualisierte Auflage, Pearson 2012. Der Kurs verwendet außerdem Material aus dem Buch von Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh: Handbook of Satisfiability, IOS Press, 2009, sowie aus den folgenden zwei Aufsätzen: Propagation via lazy clause generation, O. Ohrimenko, P. J. Stuckey und M. Codish, Constraints 14.3 (2009): 357-391 und Lazy clause generation reengineered, T. Feydy und P. J. Stuckey, International Conference on Principles and Practice of Constraint Programming (2009).
Der Kurs wird auf Englisch mit deutschen Untertiteln gehalten.
Welche Themen werden behandelt?
- Einführung in Constraint Satisfaction Problems (CSP)
- Schlussfolgerungstechniken moderner CSP-Solver-Typen
- Endliche-Domain-Propagation (verwendet von CP-Solvern)
- Konfliktgetriebene Klausellernen (verwendet von SAT-Solvern)
- Lazy Clause Generation (verwendet von CP-SAT-Solvern)
- Modellierung von Constraint Satisfaction Problems
Was werde ich erreichen?
Am Ende des Kurses werden Sie in der Lage sein,
- formell über Constraint-Satisfaction-Probleme zu sprechen,
- die Finite-Domain-Propagation und ihre Verwendung in CP-Solvern zu verstehen,
- zu verstehen, wie der Davis-Putnam-Logemann-Loveland-Algorithmus durch Klausel-Lernen zum Conflict-Driven Clause Learning Algorithm erweitert werden kann,
- zu verstehen, wie Lazy Clause Generation funktioniert und wie sie verwendet wird, um die Vorteile von CP- und SAT-Solvern in CP-SAT-Solvern zu kombinieren,
- Probleme in MiniZinc zu modellieren und die Herausforderungen guten Modellierens zu verstehen
Welche Voraussetzungen muss ich erfüllen?
Grundlagen der Künstlichen Intelligenz III: Logik und Erfüllbarkeit
