Algoritmo de Davis-Putnam

En lógica e informática , el algoritmo de Davis-Putnam fue desarrollado por Martin Davis y Hilary Putnam para verificar la validez de una fórmula de lógica de primer orden mediante 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 finaliza con fórmulas válidas. Actualmente, 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 base 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 φ basta con probar que una instancia base de ¬φ es insatisfacible. Si φ no es válida, la búsqueda de una instancia base insatisfacible no terminará.

El procedimiento para comprobar la validez de una fórmula φ consta, a grandes rasgos, de estas tres partes:

• Pon la fórmula ¬φ en forma prenexa y elimina los cuantificadores.
• generar todas las instancias de fundamento proposicional, una por una
• comprobar si cada instancia es satisfacible.
  • Si alguna instancia no se puede satisfacer, entonces indique que φ es válida. De lo contrario, continúe con la comprobación.

La última parte es un solucionador SAT basado en la resolución (como se ve en la ilustración), con un uso intensivo de la propagación de unidades y la eliminación literal pura (eliminación de cláusulas con variables que aparecen solo de forma positiva o solo de forma negativa en la fórmula).

Algoritmo DP Solucionador SAT 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 unidad: mientras Φ contenga una cláusula de unidad { l } hacer para cada cláusula c en Φ que contenga l hacer Φ ← remove-from-formula ( c , Φ); para cada cláusula c en Φ que contenga ¬ l hacer Φ ← remove-from-formula ( c , Φ); Φ ← agregar-a-la-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 cuyas ocurrencias en Φ tengan la misma polaridad , para cada cláusula c en Φ que contenga l, haga Φ ← remove-from-formula ( c , Φ); // Condiciones de parada: 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 aparezca 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 hacer // resolver c con n: r ← ( c \ { l }) ∪ ( n \ {¬ l }); Φ ← agregar-a-la-fórmula ( r , Φ); para cada cláusula c que contenga l o ¬ l hacer Φ ← eliminar-de-la-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 crecimiento exponencial, en el peor de los casos, del tamaño de la fórmula.

El algoritmo de Davis-Putnam-Logemann-Loveland es un refinamiento de 1962 del paso de satisfacibilidad proposicional del procedimiento de Davis-Putnam, que requiere 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 comprueba recursivamente si una fórmula simplificada con l asignado un valor verdadero es satisfacible o si lo es una fórmula simplificada con l asignado un valor falso. Todavía constituye la base de los solucionadores SAT completos más eficientes de la actualidad (a fecha de 2015) .

• Herbrandización
• Algoritmo DPLL

• Davis, Martin; Putnam, Hilary (1960). "Un procedimiento computacional para la teoría de la cuantificación" . Journal of the ACM . 7 (3): 201– 215. doi : 10.1145/321033.321034 .
• Davis, Martin; Logemann, George; Loveland, Donald (1962). "Un programa informático para la demostración de teoremas" . Communications of the ACM . 5 (7): 394– 397. doi : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 .
• R. Dechter; I. ​​Rish. «Resolución direccional: El procedimiento Davis-Putnam, una revisión». En J. Doyle, E. Sandewall y P. Torasso (eds.). Principios de representación del conocimiento y razonamiento: Actas de la Cuarta Conferencia Internacional (KR'94) . Kaufmann. págs. 134-145 . 
• John Harrison (2009). Manual de lógica práctica y razonamiento automatizado . Cambridge University Press. pp. 79-90 . ISBN  978-0-521-89957-4.