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.