Algoritmo de Davis-Putnam

O Algoritmo de Davis-Putnam, criado por Martin Davis e Hilary Putnam, foi um dos pioneiros na área de checagem da satisfatibilidade de uma fórmula quando essa encontra-se na Forma Normal Conjuntiva (FNC). É uma forma de resolução em que cada variável é escolhida pelo fato de se poder resolver todas as cláusulas em que a mesma está contida na sua forma positiva com qualquer cláusula em que ela encontre-se em sua forma negada.

Funcionamento

Ao invés de procurar enumerar cada combinação possível de valorações para as variáveis, esse algoritmo utiliza técnicas de backtracking para reduzir o espaço de procura. A base do algoritmo é a seguinte: se um assinalamento parcial fizer uma cláusula ser avaliada para FALSO, esse assinalamento parcial não poderá ser parte de uma solução válida. O algoritmo procura identificar a não satisfatibilidade em um assinalamento parcial de forma que não haja necessidade de tentar outras variáveis ainda sem valor atribuído. Isso normalmente resulta em uma procura mais eficiente do que simplesmente enumerar cada uma das combinações possíveis de valoração. O algoritmo é recursivo e cria uma árvore de procura, atribuindo valores e dividindo o problema em problemas menores (Divisão e Conquista). O algoritmo funciona bem na média, chegando a resultados satisfatórios para alguns tipos de problemas, porém seu pior caso, como esperado, é exponencial.