Algorisme de Davis-Putnam
From Wikipedia, the free encyclopedia
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 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 seva negació
- per a cada clàusula que continga la variable i cada clàusula que continga la negació de la variable
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.