Constraint-Programmierung
Vorlesung
Sommersemester 2009, 2012

Johannes Waldmann, HTWK Leipzig

Einleitung
- Constraint-Programmierung--Beispiel
- Industrielle Anwendungen der CP
- Industrielle Anwendungen der CP
- CP-Anwendung: Polynom-Interpretationen
- Wettbewerbe für Constraint-Solver
- Gliederung der Vorlesung
- Organisatorisches
- Literatur
Erfüllbarkeit aussagenlogischer Formeln (SAT)
- Aussagenlogik: Syntax
- Aussagenlogik: Semantik
- Der Folgerungsbegriff
- Normalformen (DNF, CNF)
- Modellierung durch SAT
- Benutzung von SAT-Solvern
- Äquivalenzen
- Erfüllbarkeits-Äquivalenz
- Tseitin-Transformation
- Tseitin-Transformation (Übung)
- Beispiele zur SAT-Modellierung
SAT: Anwendungen
- SAT-Kodierungen
- SAT-Kodierung: Independent Set
- SAT-Kodierung: Anzahl-Constraints
- SAT-Kodierung: Vertex Cover
- SAT-Kodierung: Hamiltonkreis
- SAT-Kodierung: Färbung von Graphen
- Suche nach symmetrischen Lösungen
- Neue Schranke für Van der Waerdens Funktion
Software zur SAT-Kodierung
- Überblick
- Technische Grundlagen
- Automatische Hilfsvariablen
- Realisierung logischer Funktionen
- Dekodierung mit Typklassen
- Relationen
- SAT-Solver in Paketmanagern
- Pentomino
- Schwierige Fälle für die SAT-Kodierung
SAT-Solver
- Überblick
- Evolutionäre Algorithmen für SAT
- Lokale Suche (GSat, Walksat)
- DPLL
- DPLL: Heuristiken, Modifikationen
- Beweise für Nichterfüllbarkeit
- Resolution
- Resolution und Unerfüllbarkeit
- Resolution, Bemerkungen
- DPLL: Lernen von Konfliktklauseln
- Vorverarbeitung
- Reverse Unit Propagation
Binäre Entscheidungsgraphen (ROBDDs)
- Motivation
- Darstellung von Modellmengen
- Entscheidungsbäume mit Sharing
- Eigenschaften von ROBDDs
- Operationen mit ROBDDs
- OBDD-Anwendung: Modelle zählen
- ROBBD-Implementierungen
Prädikatenlogik
- Plan
- Syntax der Prädikatenlogik
- Semantik der Prädikatenlogik
- Unentscheidbarkeit
- Folgerungen aus Unentscheidbarkeit
Termgleichungen
- Einführung
- Unifikation--Begriffe
- Unifikation--Definition
- Unifikation--Algorithmus
- Übung zur Prädikaten-Logik
- Übung zu Termgleichungen
Lineare Gleichungen und Ungleichungen
- Syntax, Semantik
- Normalformen
- Hintergründe
- Lineare Gleichungssysteme
- Lineare Ungleichungen und Optimierung
- Lösungsverfahren für lin. Ungl.-Sys.
- Fourier-Motzkin-Verfahren
- (Mixed) Integer Programming
- SAT als IP
- Travelling Salesman als MIP
- Travelling Salesman als MIP (II)
- min und max als MIP
- Übungen zu lin. Gl./Ungl.
(Integer/Real) Difference Logic
- Motivation, Definition
- Lösung von Differenz-Constraints
- Constraint-Graphen für IDL
- Kürzeste Wege in Graphen
- Lösungsidee
- Laufzeit
Polynomgleichungen
- Hilberts 10. Problem
- Probleme als Motor und Indikator des Fortschritts in der Wissenschaft
- Beispiele f. Polynomgleichungen
- Geschichte
- Polynomgleichungen über $\mathbb {R}$ mathend000#
- Quantoren-Elimination über $\mathbb {R}$ mathend000#
- Polynomgleichungen über $\mathbb {Z}$ mathend000#
- Diophantische Mengen
Presburger-Arithmetik
- Definition, Resultate
- Beispiele f. Presburger-Formeln
- Entscheidungsverfahren (Ansatz)
- Entscheidungsverfahren (Kodierung)
- Formeln und Modellmengen
- Automaten (Definition)
- Automaten (Operationen: Durchschnitt)
- Automaten (Operationen: Komplement)
- Automaten (Operationen: Projektion)
- Zusammenfassung Entscheidbarkeit
- Eine untere Schranke
- Untere Schranke
- Presburger-Arithmetik und große Zahlen
Uninterpretierte Funktionen (UF)
- Motivation, Definition
- Anwendungen
- Terme
- Gleichheit von Termen
- Die Logik QF_UF in SMT-LIB
- Ackermann-Transformation
Gleichheits-Constraints
- (Dis)Equality Constraints (Bsp, Def)
- Lösungsplan: SAT-Kodierung
- Gleichheitsgraph (equality graph)
- Vereinfachen von Formeln
- Reduktion zu Aussagenlogik (I)
- Reduktion zu Aussagenlogik (II)
- Ausflug Graphentheorie
- Kleine Welt
Testklausur KW23
- SAT, CNF, Kodierung
- ROBDD
- Lineare Ungleichungen
- Differenz-Logik
- EC/UF
- Presburger-Arithmetik (PA)
Programme mit Arrays
- Definition
- Array-Logik (Beispiel mit Quantoren)
- Array-Logik (Beispiel QF_AX)
- Array-Logik (Beispiel QF_AUFLIA)
- Definition von Array-Formeln
- Vereinfachung von Array-Formeln:
- Übung Array-Formeln/NNF
Kombination von Theorien
- Motivation
- Definition
- Konvexe Theorien
- Nelson-Oppen (I)
- Nelson-Oppen für konvexe Theorien
- Nelson-Oppen, Beispiel
SMT, DPLL(T)
- SMT
- DPLL(T)
- DPLL(T), Beispiel
- DPLL(T): Einzelheiten, Beispiele
- DPLL(T) Übung
DPLL/CDCL
- CDCL: Spezifikation
- CDCL: Implementierung, Übung
Bitblasting
- Idee
- Binäre Addition
- Subtraktion
- Vergleiche
- Multiplikation
- Bitshift
- Unärkodierung
- CNF-Kompression (Motivation)
- CNF-Kompression (Implementierung)
Zusammenfassung, Ausblick
- Kernaussagen
- Kernthemen
- Themen zum Weiterarbeiten
Über dieses Dokument ...

2014-03-31