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 Martin Davis, Hilary Putnam, George Logemann en Donald W. Loveland 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 Chaff, GRASP en BerkMin.