SAT ist ein klassisches NP-vollständiges Problem und ist im Allgemeinen nicht effizient lösbar. Dennoch gibt es Verfahren, die in vielen praktischen Anwendungen gute Ergebnisse zeigen. Vor allem in den letzten 10 Jahren wurden neue Techniken entwickelt, die ein effizientes Lösen von Formeln mit einer großen Zahl von Variablen ermöglichen.