DPLL est l’algorithme derrière les solveurs comme z3, qui permettent de résoudre des problèmes de combinaisons logique de formules dans une théorie mathématique.
À l’origine l’algorithme était de "Davis Putnam", pour décider de la satisfaction de formules booléennes (c’est à dire de savoir s’il y a moyen de rendre une formule booléenne vraie en affectant des valeurs à ses variables). C’est un algorithme de recherche arborescente.
L’algorithme a été étendu (par d’autres) pour plus d’efficacité pour donner DPLL, qui a permis de résoudre des formules SAT de grande taille efficacement au fil des ans et des optimisations des solveurs, il y a une communauté qui travaille encore dessus.
Et par dessus a été rajouté avec DPLL(T) la possibilité de résoudre des formules non plus simplement booléennes, mais dans lesquels on a remplacés les booléens par des formules d’une théories, par exemple un ensemble d’équations. La résolution des équations est déléguées à un solveur "fils" à qui on file des ensembles de formule et qui dit si cet ensemble de formule est cohérent (a une solution) ou pas. Cet algorithme a fait florès, Microsoft a développé z3 https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/ pour la communauté de la vérification logicielle entre autre, qui a eu son petit succès, autour.
Il semble cependant que si l’algorithme DP a fait florès, cette contribution est assez ignorée par la communauté mathématique qui le considère plus comme un historien de la logique.
# Le "D" de DPLL
Posté par Thomas Douillard . Évalué à 7.
DPLL est l’algorithme derrière les solveurs comme z3, qui permettent de résoudre des problèmes de combinaisons logique de formules dans une théorie mathématique.
À l’origine l’algorithme était de "Davis Putnam", pour décider de la satisfaction de formules booléennes (c’est à dire de savoir s’il y a moyen de rendre une formule booléenne vraie en affectant des valeurs à ses variables). C’est un algorithme de recherche arborescente.
L’algorithme a été étendu (par d’autres) pour plus d’efficacité pour donner DPLL, qui a permis de résoudre des formules SAT de grande taille efficacement au fil des ans et des optimisations des solveurs, il y a une communauté qui travaille encore dessus.
Et par dessus a été rajouté avec DPLL(T) la possibilité de résoudre des formules non plus simplement booléennes, mais dans lesquels on a remplacés les booléens par des formules d’une théories, par exemple un ensemble d’équations. La résolution des équations est déléguées à un solveur "fils" à qui on file des ensembles de formule et qui dit si cet ensemble de formule est cohérent (a une solution) ou pas. Cet algorithme a fait florès, Microsoft a développé z3 https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/ pour la communauté de la vérification logicielle entre autre, qui a eu son petit succès, autour.
Il semble cependant que si l’algorithme DP a fait florès, cette contribution est assez ignorée par la communauté mathématique qui le considère plus comme un historien de la logique.
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.