Davis–Putnam-algoritmus (DPLL)

Kapcsolódó könyvfejezetek: 
7.5. Hatékony ítéletkalkulus következtetés
Rövid szöveges bemutatás: 
A DPLL algoritmus az eredeti Davis-Putnam algoritmus továbbfejlesztése. Célja a kielégíthetőségi problémák vizsgálata és annak megválaszolása, hogy a probléma megoldható-e, például az adott CNF-SAT probléma megoldható-e. Ez egy visszalépéses rekurzív kereső algoritmus, melyet 1962-ben publikáltak. Az algoritmus egy CNF mondatot kezd el vizsgálni, amiből kiszűri a klózokat és szimbólumokat.