DPLL

DPLL (Davis-Putnam-Logemann-Loveland) è un algoritmo di ricerca esaustiva, basato sul backtracking, utilizzato per decidere la soddisfacibilità booleana di formule di logica proposizionale in forma normale congiuntiva (CNF), problema noto come . È stato introdotto nel 1962 da Martin Davis, Hilary Putnam, e , e rappresenta una specializzazione del precedente algoritmo di Davis-Putnam, una procedura sviluppata nel 1960. Per questo, soprattutto nelle pubblicazioni più vecchie l'algoritmo Davis-Logemann-Loveland è spesso indicato come il "metodo Davis-Putnam" o "algoritmo DP". Altre nomenclature comuni che mantengono la distinzione fra i due sono DLL e DPLL. Il DPLL è una procedura assai efficiente, e dopo più di 40 anni forma ancora la base dei più efficienti risolutori SAT completi, così come per molti dimostratori di teoremi per frammenti di logica del primo ordine.