Nächste Seite: Wdhlg. Prädikatenlogik (Syntax) Aufwärts: Constraint-Programmierung Vorlesung Sommersemester 2009 Vorherige Seite: Pseudo-Boolean Constraints

SMT (satisfiability modulo theory)

Unterabschnitte

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

2009-06-22