DPLL-Algorithmus
aus Wikipedia, der freien encyclopedia
In der Logik und Informatik ist der Davis-Putnam-Logemann-Loveland (DPLL)-Algorithmus ein vollständiger, auf Backtracking basierender Suchalgorithmus zur Bestimmung der Erfüllbarkeit von Formeln der Aussagenlogik in konjunktiver Normalform, d. h. zur Lösung des CNF-SAT-Problems.
Er wurde 1961 von Martin Davis, George Logemann und Donald W. Loveland eingeführt und ist eine Verfeinerung des früheren Davis-Putnam-Algorithmus, der ein von Davis und Hilary Putnam 1960 entwickeltes auflösungsbasiertes Verfahren ist. Vor allem in älteren Veröffentlichungen wird der Davis-Logemann-Loveland-Algorithmus oft als „Davis-Putnam-Methode“ oder „DP-Algorithmus“ bezeichnet. Andere gebräuchliche Bezeichnungen, die diese Unterscheidung beibehalten, sind DLL und DPLL.