Algorisme de Davis-Putnam

L'algorisme de Davis-Putnam va ser desenvolupat per Martin Davis i Hilary Putnam per comprovar la satisfacibilitat de les fórmules de la lògica proposicional en forma normal conjuntiva, és a dir, en conjunts de clàusules. Això és una forma de resolució en la qual les variables són triades iterativament i eliminades mitjançant la resolució de cada clàusula en la qual la variable apareix afirmada amb una clàusula en la qual la variable és negada.

L'algorisme és així:

• per a cada variable en la fórmula
  • per a cada clàusula ${\displaystyle c}$ que continga la variable i cada clàusula ${\displaystyle n}$ que continga la negació de la variable
    • resoldre ${\displaystyle c}$ i ${\displaystyle n}$ i afegir la resolució a la fórmula
  • eliminar totes les clàusules originals que continguen la variable o la seva negació

El nom algorisme Davis-Putnam o algorisme DP de vegades és emprat incorrectament per referir-se a l'algorisme DPLL, el qual està relacionat però és diferent.

Referències

• Davis, Martin; Putnam, Hillary «A Computing Procedure for Quantification Theory». Journal of the ACM, 7, 1, 1960, pàg. 201–215.

• Davis, Martin; Logemann; Loveland, Donald «A Machine Program for Theorem Proving». Communications of the ACM, 5, 7, 1962, pàg. 394–397.

• 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.