DPLL-algoritme

Het DPLL-algoritme (Davis-Putnam-Logemann-Loveland algoritme) is een algoritme voor het onderzoeken van de vervulbaarheid van een propositie in conjunctieve normaalvorm (dit probleem is ook bekend als CNF-SAT). Het algoritme werd gepubliceerd in 1962 door , Hilary Putnam, en als een verbetering van een eerder algoritme van Davis en Putnam uit 1960. Het algoritme maakt gebruik van backtracking indien nodig. Er bestaan allerlei verbeterde varianten van het DPLL-algoritme, zoals het , en .