Algoritmo DPLL

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.