DPLL(T), Beispiel

T = mathend000# LRA (linear real arithmetic)

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

DPLL(T) benutzt



2014-03-31