Algoritmo de Davis-Putnam
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 de primer orden válidas 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 insatisfactoria tiene una instancia base insatisfactoria , y en el hecho de que una fórmula es válida si y solo si su negación es insatisfactoria. Tomados en conjunto, estos hechos implican que para probar la validez de φ es suficiente probar que una instancia fundamental de ¬φ es insatisfactoria. Si φ no es válido, la búsqueda de un caso de terreno insatisfactorio 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 de unidades 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 equisatisfacible , 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 de Davis-Putnam-Logemann-Loveland es un refinamiento de 1962 del paso de satisfacibilidad proposicional del procedimiento de 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 satisfactoria o si una fórmula simplificada con l asignado falso lo es. Todavía forma la base de los solucionadores de SAT completos más eficientes de la actualidad (a partir de 2015) .
