Algorithme de davis-putnam

Algorithme de davis-putnam

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.

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 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}))

Voir aussi

  • Portail de la logique Portail de la logique
  • Portail de l’informatique Portail de l’informatique
Ce document provient de « Algorithme de Davis-Putnam ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Algorithme de davis-putnam de Wikipédia en français (auteurs)

Игры ⚽ Поможем сделать НИР

Regardez d'autres dictionnaires:

  • 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… …   Wikipédia en Français

  • 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… …   Wikipédia en Français

  • Davis-Putnam — 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… …   Wikipédia en Français

  • Méthode de Davis-Putnam — 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… …   Wikipédia en Français

  • Davis — Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom. Cet article possède des paronymes, voir : Davies et Davy. Le nom Davis peut désigner des personnes (nom de famill …   Wikipédia en Français

  • Procédure de David-Putnam — 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… …   Wikipédia en Français

  • Hilary Putnam — Pour les articles homonymes, voir Putnam. Hilary Putnam Philosophe Époque contemporaine …   Wikipédia en Français

  • Hilary Whitehall Putnam — Hilary Putnam Pour les articles homonymes, voir Putnam. Hilary Putnam Philosophe Époque contemporaine …   Wikipédia en Français

  • Problème SAT — On nomme problème SAT un problème de décision visant à savoir s il existe une solution à une série d équations logiques données. En termes plus précis : une évaluation sur un ensemble de variables propositionnelles[1] telle qu une formule… …   Wikipédia en Français

  • Probleme SAT — Problème SAT On nomme problème SAT un problème de décision visant à savoir s il existe une solution à une série d équations logiques données. En termes plus précis : une valuation sur un ensemble de variables propositionnelles[1] telle qu… …   Wikipédia en Français

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”