Algoritmo di Davis-Putnam

Da Wikipedia, l'enciclopedia libera.

L'algoritmo di Davis-Putnam fu sviluppato da Martin Davis e Hilary Putnam allo scopo di verificare la soddisfacibilità booleana di formule di logica proposizionale in forma normale congiuntiva (CNF). È un tipo di procedimento di risoluzione nel quale le variabili sono scelte iterativamente ed eliminate, risolvendo ogni clausola in cui questa compaia diretta con ogni clausola in cui compaia negata.

L'algoritmo funziona come espresso di seguito:

  • per ogni variabile nella formula
    • per ogni clausola c contenente la variabile e per ogni clausola n contenente la negazione della variabile
      • risolvi c e n e aggiungi il risolvente nella formula
    • rimuovi tutte le clausole originarie che contenevano la variabile diretta o negata

Il nome Davis–Putnam o DP è a volte scorrettamente usato in riferimento al correlato ma distinto algoritmo DPLL.

Fonti[modifica | modifica wikitesto]

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