W tej sekcji opisujemy dwie rodziny wydajnych algorytmów do ogólnego wnioskowania o zdarzeniu opartego na sprawdzaniu modelu: jedno podejście oparte na przeszukiwaniu wstecznym, a drugie na przeszukiwaniu lokalnego wznoszenia. Algorytmy te są częścią „technologii” logiki zdań. Opisane przez nas algorytmy służą do sprawdzania spełnialności: problem SAT. (Jak zauważono, przeprowadzenie testów α|= β można przeprowadzić testując niespełnienie wyników α Λ ¬β beta.
Wspomnieliśmy o związku między znalezieniem satysfakcjonującego modelu dla zdania logicznego a znalezieniem rozwiązania problemu spełniania ograniczeń, więc być może nie jest zaskakujące, że dwie rodziny algorytmów spełnialności zdań bardzo przypominają algorytmy wycofywania i lokalne algorytmy wyszukiwania. Są one jednak same w sobie niezwykle ważne, ponieważ wiele kombinatorycznych problemów w informatyce można sprowadzić do sprawdzenia spełnialności zdania zdaniowego. Każde ulepszenie algorytmów spełnialności ma ogromne konsekwencje dla naszej ogólnej zdolności do radzenia sobie ze złożonością.