Nächste Seite: SMT = Satisfiability modulo Aufwärts: Constraint-Programmierung Vorlesung Sommersemester 2009, Vorherige Seite: Presburger-Arithmetik und große Zahlen

SMT, DPLL(T)

Unterabschnitte

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

2014-07-06