b'\n_START_ARTICLE_\nAlgoritmo de Davis-Putnam\n_START_PARAGRAPH_\nO Algoritmo de Davis-Putnam, criado por Martin Davis e Hilary Putnam, foi um dos pioneiros na \xc3\xa1rea de checagem da satisfatibilidade de uma f\xc3\xb3rmula quando essa encontra-se na Forma Normal Conjuntiva (FNC). \xc3\x89 uma forma de resolu\xc3\xa7\xc3\xa3o em que cada vari\xc3\xa1vel \xc3\xa9 escolhida pelo fato de se poder resolver todas as cl\xc3\xa1usulas em que a mesma est\xc3\xa1 contida na sua forma positiva com qualquer cl\xc3\xa1usula em que ela encontre-se em sua forma negada.\n_START_SECTION_\nFuncionamento\n_START_PARAGRAPH_\nAo inv\xc3\xa9s de procurar enumerar cada combina\xc3\xa7\xc3\xa3o poss\xc3\xadvel de valora\xc3\xa7\xc3\xb5es para as vari\xc3\xa1veis, esse algoritmo utiliza t\xc3\xa9cnicas de backtracking para reduzir o espa\xc3\xa7o de procura. A base do algoritmo \xc3\xa9 a seguinte: se um assinalamento parcial fizer uma cl\xc3\xa1usula ser avaliada para FALSO, esse assinalamento parcial n\xc3\xa3o poder\xc3\xa1 ser parte de uma solu\xc3\xa7\xc3\xa3o v\xc3\xa1lida. O algoritmo procura identificar a n\xc3\xa3o satisfatibilidade em um assinalamento parcial de forma que n\xc3\xa3o haja necessidade de tentar outras vari\xc3\xa1veis ainda sem valor atribu\xc3\xaddo. Isso normalmente resulta em uma procura mais eficiente do que simplesmente enumerar cada uma das combina\xc3\xa7\xc3\xb5es poss\xc3\xadveis de valora\xc3\xa7\xc3\xa3o. O algoritmo \xc3\xa9 recursivo e cria uma \xc3\xa1rvore de procura, atribuindo valores e dividindo o problema em problemas menores (Divis\xc3\xa3o e Conquista). O algoritmo funciona bem na m\xc3\xa9dia, chegando a resultados satisfat\xc3\xb3rios para alguns tipos de problemas, por\xc3\xa9m seu pior caso, como esperado, \xc3\xa9 exponencial.'