Méthode de Davis-Putnam
- 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 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
Voir aussi
Portail de la logique
Portail de l’informatique
Catégories : Algorithme | Logique
Wikimedia Foundation.
2010.
Contenu soumis à la licence CC-BY-SA. Source : Article Méthode de Davis-Putnam de Wikipédia en français (auteurs)
Regardez d'autres dictionnaires:
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
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
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 — 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
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
SAT (problème) — 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
Sat4j — 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
