Algoritme de Davis-Putnam
El algoritme de Davis-Putnam va ser desenrollat per Martin Davis i Hilary Putnam per a comprovar la satisfacibilidad de les fòrmules de la llògica proposicional en forma normal conjuntiva, és dir, en conjunts de clàusules. Açò és una forma de resolució en la qual les variables són elegides iterativamente i eliminades per mig de la resolució de cada clàusula en la que la variable apareix afirmada en una clàusula en la que la variable és negada.
L'algoritme és com seguix:
- per a cada variable en la fòrmula
- per a cada clàusula que continga la variable i cada clàusula que continga la negació de la variable
- resoldre i i afegir la resolució a la fòrmula
- eliminar totes les clàusules originals que continguen la variable o la seua negació
- per a cada clàusula que continga la variable i cada clàusula que continga la negació de la variable
El nom algoritme Davis-Putnam o algoritme DP a voltes és amprat incorrectament per a referir-se al algoritme DPLL, el qual està relacionat pero és diferent.
Referències
[editar | editar còdic]- 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), pp. 134-145, 1994.
- Este artícul conté una traducció derivada de «Algoritmo de Davis-Putnam» de Wikipedia en castellà publicada baix la Llicència de documentació lliure de GNU i la Llicència Creative Commons Reconeiximent-CompartirIgual 4.0 Internacional.