Algorithme de Davis-Putnam

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

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)[modifier | modifier le code]

Cet algorithme est essentiellement une boucle sur l'application de trois règles, dont les deux premières se retrouvent dans l'algorithme DPLL.

La propagation unitaire[modifier | modifier le code]

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[modifier | modifier le code]

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[modifier | modifier le code]

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[modifier | modifier le code]

On part des clauses initiales C_1 = \neg a \vee c\ ;\ C_2 = a \vee c\ ;\ C_3 = b \vee \neg c\ ;\ C_4 = a \vee \neg b \vee c\ ;\ C_5 = \neg b \vee \neg c\ ;\ C_6 = \neg a \vee \neg b \vee \neg c\ ;\ C_7 = a \vee \neg d\ ;\ C_8 = b \vee \neg d.

On voit tout de suite que \neg d est un littéral pur, on peut donc supprimer C_7 et C_8 de l'ensemble des clauses.

Ensuite, on doit appliquer l'étape de résolution, sur a par exemple, ce qui donne les nouvelles clauses C_{1,2} = c et C_{1,4} = \neg b \vee c (C_{2,6} et C_{4,6} étant des tautologies) et permet de supprimer les clauses C_1, C_2, C_4, C_6.

La clause C_{1,2} est unitaire, permet de supprimer C_{1,4} et de transformer C_3 et C_5 en C'_3 = b et C'_5 = \neg b. 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[modifier | modifier le code]

Références[modifier | modifier le code]