Ansatz: für jede elementare Formel F = P(t1,..., tk) eine neue boolesche Unbekannte pF F, dann SAT-Problem für die p* lösen.
Ideen:
Übersichtsvortrag: Robert Nievenhuis et al. http://www.lsi.upc.edu/~roberto/RTA07-slides.pdf