Algorithme de Davis-Putnam
En calcul propositionnel, l'algorithme de Davis-Putnam est une méthode de détermination de la satisfiabilité d'une formule en forme normale conjonctive, c'est-à-dire une conjonction de clauses (disjonctions de littéraux). Il a été développé par Martin Davis et Hilary Putnam. Cet algorithme a d'abord été conçu pour l'obtention automatique de preuves en calcul des prédicats, mais sa principale innovation concerne la réfutation automatique d'un ensemble de clauses.
Comme son dérivé plus connu, l'algorithme DPLL, l'algorithme de Davis-Putnam utilise la propagation unitaire et l'élimination des littéraux purs. Mais l'appel récursif utilisé dans l'algorithme DPLL est remplacé par l'utilisation exhaustive de la règle de résolution sur une variable. L'algorithme de Davis-Putnam permet de prouver qu'un ensemble de clauses est satisfiable (ou non), mais contrairement à l'algorithme DPLL, il ne donne pas directement une affectation satisfaisant cet ensemble de clauses.
Description de l'algorithme (pour la logique propositionnelle)
Cet algorithme est essentiellement une boucle sur l'application de trois règles, dont les deux premières se retrouvent dans l'algorithme DPLL. On observera que chaque règle transforme une formule de départ (disons f) en une autre formule f' (ayant moins de littéraux) avec la garantie que la non-satisfiabilité de f' implique la non-satisfiabilité de f. Ainsi l'algorithme termine (puisque le nombre de variables est fini) et par transitivité la non-satisfiabilité de la formule finale implique celle de la formule donnée en entrée.
La propagation unitaire
Pour chaque clause unitaire (ne contenant qu'un littéral), on supprime les clauses comprenant ce littéral, et on enlève le littéral opposé des autres clauses. Par exemple, une clause x montre que x est vrai, on peut supprimer toutes les clauses de la forme A ∨ x et supprimer tous les ¬ x des autres clauses. Cette règle peut se répéter jusqu'à ce qu'il ne reste plus de clause unitaire.
L'élimination des littéraux purs
Si une variable apparaît exclusivement sous la forme de littéral positif (ou de littéral négatif) dans l'ensemble de clauses, on peut supprimer toutes les clauses dans laquelle elle apparaît. Par exemple, si on ne trouve aucune clause de la forme ¬ x, toutes les clauses de la forme A ∨ x peuvent être supprimées. Là encore, cette règle peut se répéter et se combiner.
Résolution exhaustive pour une variable
Cette règle n'est appliquée que lorsque les deux autres ne sont plus possibles. Dans ce cas on choisit une variable (par exemple x) et on applique la règle de résolution sur toutes les clauses utilisant x : à partir d'une clause A ∨ x et d'une clause B ∨ ¬ x, on génère la clause A ∨ B (si celle-ci n'est pas une tautologie, c'est-à-dire ne comprend pas à la fois y et ¬ y). Ensuite, on supprime de l'ensemble de clauses toutes les clauses utilisant la variable x.
On voit que l'application de chaque règle fait décroître le nombre de variables (même si la résolution peut augmenter le nombre de clauses), ce qui garantit la terminaison de l'algorithme. L'algorithme se termine lorsque l'ensemble de clauses est vide (l'ensemble initial est satisfiable) ou lorsqu'une clause vide (contradictoire) apparaît (l'ensemble initial est insatisfiable).
Exemple
On part des clauses initiales .
On voit tout de suite que est un littéral pur, on peut donc supprimer et de l'ensemble des clauses.
Ensuite, on doit appliquer l'étape de résolution, sur a par exemple, ce qui donne les nouvelles clauses et ( et étant des tautologies) et permet de supprimer les clauses .
La clause est unitaire, permet de supprimer et de transformer et en et . Enfin, l'étape de résolution appliqué sur b (dernière variable restante) crée une clause contradictoire, ce qui montre que l'ensemble de clauses initiale est insatisfiable.
Voir aussi
Références
- (en) Martin Davis et Hilary Putnam, « A Computing Procedure for Quantification Theory », Journal of the ACM, vol. 7, no 3, , p. 201–215 (DOI 10.1145/321033.321034, lire en ligne).
Portail de l'informatique théorique 
Portail de la logique