Nächste Seite:
Einleitung
Constraint-Programmierung
Vorlesung
Sommersemester 2009
Johannes Waldmann, HTWK Leipzig
Einleitung
Organisatorisches
Gliederung
Projektthemen
Erfüllbarkeit aussagenlogischer Formeln (SAT)
Aussagenlogik: Syntax
Aussagenlogik: Semantik
Normalformen (DNF, CNF)
Erfüllbarkeits-Äquivalenz
Tseitin-Transformation
Tseitin-Transpormation (Übung)
Software zur SAT-Kodierung
Überblick
CNF, Solver
Automatische Hilfsvariablen
Realisierung logischer Funktionen
Dekodierung mit Typklassen
Relationen
Anwendung: Graphen
SAT-Kodierung von Binärzahlen
SAT: Anwendungen
SAT-Kodierungen
SAT-Kodierung: Independent Set
SAT-Kodierung: Anzahl-Constraints
SAT-Kodierung: Vertex Cover
SAT-Kodierung: Hamiltonkreis
Suche nach symmetrischen Lösungen
Neue Schranke für Van der Waerdens Funktion
SAT-Solver
Überblick
Evolutionäre Algorithmen für SAT
Lokale Suche (GSat, Walksat)
DPLL
DPLL: Heuristiken
DPLL: Konfliktklauseln
unsat, Resolution
SAT: Erweiterungen
Quantifizierte Boolesche Formeln
QBF-Beispiele mit fester Quantortiefe
Zweipersonenspiele
Komplexität
Lösung
Satz von Savitch
Pseudo-Boolean Constraints
SMT (satisfiability modulo theory)
Wdhlg. Prädikatenlogik (Syntax)
Prädikatenlogik (Semantik)
Theorien
Lineare Gleichungen
Lineare Ungleichungen
Verfahren nach Fourier und Motzkin (I)
Verfahren nach Fourier und Motzkin (II)
Weitere Verfahren für Lin. Ungl.
Implementierungen
(Un)Gl. zwischen Polynomen
Fourier-Motzkin für SAT?
Erweiterungen
Mixed Integer Programming
Anwendungsaufgabe
Ordnungsconstraints für Matrizen
Lösungsansätze
Max/Min als MIP
DPLL(T)
DPLL(T), Beispiel
Bitblasting
Idee
Binäre Addition
Subtraktion
Vergleiche
Multiplikation
Bitshift
Unärkodierung
CNF-Kompression (Motivation)
CNF-Kompression (Implementierung)
(Integer/Real) Difference Logic
Motivation, Definition
Lösung von Differenz-Constraints
Constraint-Graphen für IDL
Kürzeste Wege in Graphen
Lösungsidee
Laufzeit
Anwendung: Min/Max-Matrixungleichungen
Binäre Entscheidungsgraphen (ROBDDs)
Motivation
Darstellung von Modellmengen
Entscheidungsbäume mit Sharing
Eigenschaften von ROBDDs
Operationen mit ROBDDs
OBDD-Anwendung: Modelle zählen
Konsistenz-Begriffe
Finite-Domain-Constraints (FD)
FD-Lösungsverfahren
Konsistenzen (Überblick)
Knotenkonsistenz
Kantenkonsistenz
Pfadkonsistenz
k
-Konsistenz
Konsistenz unter Kodierungen
Gleichheits-Constraints
(Dis)Equality Constraints (Bsp, Def)
Gleichheitsgraph (equality graph)
Vereinfachen von Formeln
Reduktion zu Aussagenlogik (I)
Reduktion zu Aussagenlogik (II)
Ausflug Graphentheorie
Kleine Welt
Uninterpretierte Funktionen (UF)
Motivation, Definition
Terme
Gleichheit von Termen
Logik und Unentscheidbarkeit (I)
Logik und Unentscheidbarkeit (II)
Entscheidbare Fälle
Ackermann-Transformation
Kombination von Theorien
Motivation
Definition
Konvexe Theorien
Nelson-Oppen (I)
Nelson-Oppen für konvexe Theorien
Nelson-Oppen für nicht konvexe Theorien
Programme mit Arrays
Definition
Store entfernen
Spezialfälle
Über dieses Dokument ...
2009-06-22