DPLL(T)

Ansatz: für jede elementare Formel F = P(t1,..., tk)
eine neue boolesche Unbekannte pF $ \leftrightarrow$ F,
dann SAT-Problem für die p* lösen.

Ideen:

(optimized lazy approach)


Übersichtsvortrag: Robert Nievenhuis et al. http://www.lsi.upc.edu/~roberto/RTA07-slides.pdf



2009-06-22