Algoritmo de Davis-Putnam

Algoritmo de Davis-Putnam

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 que la variable aparece afirmada con una cláusula en la que la variable es negada.

El algoritmo es como sigue:

  • para cada variable en la fórmula
    • para cada cláusula c que contenga la variable y cada cláusula n que contenga la negación de la variable
      • resolver c y n y añadir la resolución a la fórmula
    • eliminar todas las cláusulas originales que contengan la variable o su negación

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.

Referencias

  • R. Dechter and I. Rish. Directional resolution: The Davis-Putnam procedure, revisited. In Proceedings of the Fourth International Conference on the Principles of Knowledge Representation and Reasoning (KR'94), pages 134–145, 1994.

Wikimedia foundation. 2010.

Игры ⚽ Поможем решить контрольную работу

Mira otros diccionarios:

  • Algoritmo DPLL — El algoritmo DPLL/Davis Putnam Logemann Loveland es un algoritmo completo basado en la vuelta atrás que sirve para decidir la satisfacibilidad de las fórmulas de lógica proposicional en una forma normal conjuntiva, es decir, para resolver el… …   Wikipedia Español

  • Hilary Putnam — Retrato de Putnam. Hilary Whitehall Putnam (nacido el 31 de julio de 1926, en Chicago (Illinois)) es u …   Wikipedia Español

  • Martin Davis — Nombre Martin David Davis …   Wikipedia Español

  • Problema de satisfacibilidad booleana — Saltar a navegación, búsqueda En teoría de la complejidad computacional, el Problema de satisfacibilidad booleana (SAT) fue el primer problema identificado como perteneciente a la clase de complejidad NP completo. Se trata de un problema donde… …   Wikipedia Español

  • Décimo problema de Hilbert — Saltar a navegación, búsqueda El décimo problema de Hilbert es uno de los veintitrés que David Hilbert propuso al término del siglo XIX. Su enunciado original es: Dada una ecuación diofántica con cualquier número de incógnitas y con coeficientes… …   Wikipedia Español

Compartir el artículo y extractos

Link directo
Do a right-click on the link above
and select “Copy Link”