Un article de Wikipédia, l'encyclopédie libre.

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.

[] 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

[] Algorithme Récursif

DP(T)

• Si T est vide alors retourner 1
• Si T est la clause vide alors retourner 0
• Choisir une variable Xi dans T
• retourner DP(T(Xi<-1)) U DP(T(Xi<-0))

[] Voir aussi

• Clause de Horn

 

Réagissez

Commentez l'encyclopédie:
Attention! tous les commentaites inaproprié seront supprimés

Titre:
Video YouTube ou google:	(doit être en rapport avec le sujet)
Votre mail:	(ne sera pas affiché sur le site)
Un pseudo:
Votre site:
Commentaire	(le html n'est pas autorisé, nombre de caractère maximum = 400)
	(Comment eBabylone 1.0 beta)

Le Texte ci-dessus est disponible sous GNU Free Documentation License.
La source est wikipedia http://fr.wikipedia.org/wiki/ Algorithme de Davis-Putnam