Algorithme de Davis-Putnam

Un article de Wikipédia, l'encyclopédie libre.
Cet article est une ébauche concernant les mathématiques.
Vous pouvez partager vos connaissances en l’améliorant. (Comment ?).

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.

[modifier] Algorithme

  • pour chaque variable dans la formule
    • pour chaque clause C contenant la variable et chaque clause N contenant la négation de cette variable
      • résoudre C et N et ajouter la solution à la formule
    • retirer les clauses contenant la variable ou sa négation

[modifier] Algorithme récursif

DP(T)

  • Si T est vide alors retourner Vrai
  • Si T est la clause vide alors retourner Faux
  • Choisir une variable Xi dans T
  • retourner \text{DP}(T(X_i \leftarrow \text{Vrai})) \cup \text{DP}(T(X_i \leftarrow \text{Faux}))

[modifier] Voir aussi