Algoritmo de Davis-Putnam
El algoritmo de Davis-Putnam fue desarrollado por Martin Davis y Hilary Putnam para la comprobación de la validez de una lógica de primer orden fórmula utilizando una resolución procedimiento de toma poblacionales para la lógica de proposiciones . 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 utiliza a menudo como sinónimo del procedimiento de decisión proposicional basado en la 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 insatisfactorio tiene una instancia base insatisfactorio , y en el hecho de que una fórmula es válida si y solo si su negación es insatisfactorio. Tomados en conjunto, estos hechos implican que para probar la validez de φ es suficiente probar que una instancia básica de ¬φ no es satisfactoria. Si φ no es válido, la búsqueda de una instancia de tierra insatisfactoria no terminará.
La última parte es un solucionador SAT basado en resolución (como se ve en la ilustración), con un uso ávido de propagación unitaria y eliminación literal pura (eliminación de cláusulas con variables de una sola polaridad en la fórmula). [ aclaración necesaria ]
En cada paso del solucionador SAT, la fórmula intermedia generada es igual de satisfactoria , pero posiblemente no equivalente , a la fórmula original. El paso de resolución conduce a una explosión exponencial en el peor de los casos en el 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 sólo 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 de forma recursiva si una fórmula simplificada con l asignado un valor verdadero es satisfactoria o si una fórmula simplificada con l asignado falso lo es. Todavía forma la base para los solucionadores SAT completos más eficientes de hoy (a partir de 2015) .
