algoritmo di Davis-Putnam

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 DP è stato il primo algoritmo per la risoluzione di problemi SAT . Ma questo in generale è molto inefficiente poiché richiede un uso esponenziale della memoria, quindi è adatto a problemi di piccole dimensioni. La sua evoluzione è un algoritmo di ricerca chiamato DPLL. A volte l'algoritmo di Davis–Putnam o DP è scorrettamente usato in riferimento DPLL, ma questi due sono ben distinti.