El algoritmo de Davis-Putnam fue desarrollado por Martin Davis y Hilary Putnam para comprobar la satisfacibilidad de las fórmulas de la lógica proposicional en forma normal conjuntiva, es decir, en conjuntos de cláusulas. Esto es una forma de resolución en la cual las variables son elegidas iterativamente y eliminadas mediante la resolución de cada cláusula en la que la variable aparece afirmada con una cláusula en la que la variable es negada.
El algoritmo es como sigue:
El nombre algoritmo Davis-Putnam o algoritmo DP a veces es empleado incorrectamente para referirse al algoritmo DPLL, el cual está relacionado pero es diferente.
Escribe un comentario o lo que quieras sobre Algoritmo de Davis-Putnam (directo, no tienes que registrarte)
Comentarios
(de más nuevos a más antiguos)