DPLL(T), Beispiel

T = LRA (linear real arithmetic)

durch Tseitin-Transformation als CNF darstellen (zusätzliche boolesche Variablen)

DPLL(T) benutzt



2009-06-22