Back Algorisme DPLL Catalan DPLL-Algorithmus German DPLL algorithm English Algoritmo DPLL Spanish الگوریتم DPLL Persian Algorithme DPLL French DPLL algoritmus Hungarian DPLL Italian DPLLアルゴリズム Japanese DPLL-algoritme Dutch
O algoritmo DPLL/Davis-Putnam-Logemann-Loveland é um algoritmo completo baseado em backtracking (re-leitura ou voltar atrás) para decidir a satisfatibilidade das fórmulas de lógica proposicional na forma normal clausal, isto é, para solucionar o problema SAT.
O algoritmo foi introduzido em 1962 por Martin Davis, Hilary Putnam, George Logemann e Donald W. Loveland, sendo um refinamento do algoritmo de Davis-Putnam mais antigo, o qual é baseado num processo de resolução desenvolvido por Davis e Putnam em 1960. Principalmente em publicações antigas, o algoritmo de Davis-Logemann-Loveland é freqüentemente referenciado como “O Método Davis-Putnam” ou o “Algoritmo DP”. Outros nomes comuns que mantém a distinção são DLL e DPLL.
DPLL é um procedimento altamente eficiente, e forma a base para os mais eficientes solucionadores SAT e outros problemas NP-completos que podem ser reduzidos para o problema SAT, e também para muitos provadores de teoremas para os fragmentos da lógica de primeira ordem.