En lógica y ciencias de la computación , el algoritmo de Davis-Putnam fue desarrollado por Martin Davis y Hilary Putnam para verificar la validez de una fórmula lógica de primer orden utilizando un procedimiento de decisión basado en resolución para lógica proposicional . Dado que el conjunto de fórmulas válidas de primer orden es recursivamente enumerable pero no recursivo , no existe un algoritmo general para resolver este problema. Por lo tanto, el algoritmo de Davis-Putnam solo termina en fórmulas válidas. Hoy en día, el término "algoritmo de Davis-Putnam" se usa a menudo como sinónimo del procedimiento de decisión proposicional basado en resolución ( procedimiento de Davis-Putnam ) que en realidad es solo uno de los pasos del algoritmo original.
El procedimiento se basa en el teorema de Herbrand , que implica que una fórmula insatisfacible tiene una instancia básica insatisfacible , y en el hecho de que una fórmula es válida si y solo si su negación es insatisfacible. En conjunto, estos hechos implican que para probar la validez de φ es suficiente probar que una instancia básica de ¬φ es insatisfacible. Si φ no es válida, entonces la búsqueda de una instancia básica insatisfacible no terminará.
El procedimiento para comprobar la validez de una fórmula φ consta aproximadamente de estas tres partes:
La última parte es un solucionador SAT basado en resolución (como se ve en la ilustración), con un uso entusiasta de la propagación de unidades y la eliminación literal pura (eliminación de cláusulas con variables que ocurren solo positivamente o solo negativamente en la fórmula). [ aclaración necesaria ]
Algoritmo DP SAT solucionador Entrada: Un conjunto de cláusulas Φ. Salida: Un valor de verdad: verdadero si Φ puede satisfacerse, falso en caso contrario.
función DP-SAT(Φ) repetir // propagación de la unidad: mientras Φ contiene una cláusula de unidad { l } hacer para cada cláusula c en Φ que contiene l hacer Φ ← remove-from-formula ( c , Φ); para cada cláusula c en Φ que contiene ¬ l hacer Φ ← remove-from-formula ( c , Φ); Φ ← suma-a-fórmula ( c \ {¬ l }, Φ); // eliminar cláusulas que no están en forma normal: para cada cláusula c en Φ que contenga tanto un literal l como su negación ¬ l hacer Φ ← remove-from-formula ( c , Φ); // eliminación literal pura: mientras haya un literal l, todas cuyas ocurrencias en Φ tienen la misma polaridad , hacer para cada cláusula c en Φ que contiene l hacer Φ ← remove-from-formula ( c , Φ); // condiciones de detención: si Φ está vacío, entonces devuelve verdadero; si Φ contiene una cláusula vacía, entonces devuelve falso; // Procedimiento de Davis-Putnam: elige un literal l que ocurra con ambas polaridades en Φ para cada cláusula c en Φ que contenga l y cada cláusula n en Φ que contenga su negación ¬ l // resuelve c con n: r ← ( c \ { l }) ∪ ( n \ {¬ l }); Φ ← añadir-a-fórmula ( r , Φ); para cada cláusula c que contenga l o ¬ l hacer Φ ← quitar-de-fórmula ( c , Φ); En cada paso del solucionador SAT, la fórmula intermedia generada es equisatisfacible , pero posiblemente no equivalente , a la fórmula original. El paso de resolución conduce a un aumento exponencial en el peor de los casos del tamaño de la fórmula.
El algoritmo Davis–Putnam–Logemann–Loveland es un refinamiento de 1962 del paso de satisfacibilidad proposicional del procedimiento Davis–Putnam que requiere solo una cantidad lineal de memoria en el peor de los casos. Evita la resolución de la regla de división : un algoritmo de retroceso que elige un literal l y luego verifica recursivamente si una fórmula simplificada con l asignado un valor verdadero es satisfacible o si una fórmula simplificada con l asignado falso lo es. Todavía forma la base de los solucionadores SAT completos más eficientes de la actualidad (a partir de 2015) .