Nächste Seite:
Einleitung
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-Begriffe
DPLL-Algorithmus
DPLL-Beispiel
DPLL-Beispiel (Lösung)
DPLL: Heuristiken, Modifikationen
DPLL mit CDCL (Plan)
DPLL mit CDCL (Einzelheiten)
UnSAT-Solver
Beweise für Nichterfüllbarkeit
Resolution
Resolution als Inferenzsystem
Resolution und Unerfüllbarkeit
Resolution, Bemerkungen
Vorverarbeitung
Reverse Unit Propagation
Binäre Entscheidungsgraphen (ROBDDs)
Motivation: aussagenlog. Formeln
Darstellung von Modellmengen
Entscheidungsgraphen mit Sharing
Eigenschaften von ROBDDs
Beispiele, Einfluß der Variablenordnung
Operationen mit ROBDDs (Plan)
Operationen mit ROBDDs (Implementierung)
ROBDD-Anwendungen: Modelle zählen
ROBBD-Implementierungen
Übung BDD
Prädikatenlogik
Plan
Syntax der Prädikatenlogik
Semantik der Prädikatenlogik
Theorien
Unentscheidbarkeit
Folgerungen aus Unentscheidbarkeit
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
Quantoren-Elimination über
Polynomgleichungen über
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
SMT, DPLL(T)
SMT
=
Satisfiability modulo Theory
SMT-{LIB,COMP}
Beispiel
queen10-1.smt2
aus SMT-LIB
Umfang der Benchmarks (2014)
DPLL(T), Prinzip
DPLL(T), Beispiel QF_LRA
DPLL(T): Einzelheiten, Beispiele
Übung DPLL(T)
Übung SMT-LIB
Finite Domain Constraints
Einleitung, Definition
CNF-SAT als FD-Constraint-Problem
Algorithmen für FD-Solver (Ansatz)
Lösungen, Lösbarkeit
Algorithmen für FD-Solver
Globale und lokale Konsistenz
Kantenkonsistenz (Definition)
Kantenkonsistenz (Herstellung)
Hyperkantenkonsistenz
Hyperkantenkonsistenz und Konflikte
Hyperkantenkonsistenz: Erweiterungen
Übung Konsistenz
FD und SAT
Bitblasting
Idee
Binäre Addition
Subtraktion
Vergleiche
Multiplikation
Bitshift
Unärkodierung
CNF-Kompression (Motivation)
CNF-Kompression (Implementierung)
Über dieses Dokument ...
2014-07-06
