|
Algorithme DPLLEn informatique, l'algorithme de Davis–Putnam–Logemann–Loveland (DPLL) est un algorithme de backtracking, complet, de résolution du problème SAT. Le problème SAT est un problème important à la fois d'un point de vue théorique, en particulier en théorie de la complexité où il est le premier problème prouvé NP-complet et pratique puisqu'il peut apparaître lors de la résolution de problèmes de planification classique, model checking, ou encore diagnostic et jusqu'au configurateur d'un PC ou de son système d'exploitation[réf. nécessaire]. HistoriqueIl a été introduit en 1962 par Martin Davis, Hilary Putnam, George Logemann et Donald Loveland (en). C'est une extension de l'algorithme de Davis-Putnam, une procédure développée par Davis et Putnam en 1960 basée sur l'utilisation de la règle de résolution. Dans les premières publications sur ce sujet, l'algorithme DPLL est souvent appelé « Davis Putnam method » (« méthode de Davis Putnam ») ou « DP algorithm », ou encore DLL. DPLL est une procédure hautement efficace et est toujours aujourd'hui, 50 ans après, à la base de la plupart des solveurs SAT complets modernes. Il est aussi au cœur de nombreux prouveurs automatiques de théorèmes pour des sous ensembles de la logique du premier ordre[1]. Implémentations et applicationsLe problème SAT fait l'objet de beaucoup de recherches, et des compétitions entre solveurs[2] sont organisées. Des implémentations modernes de DPLL comme Chaff et zChaff (en)[3],[4], le solveur SAT GRASP (en) ou encore Minisat [5] font partie des vainqueurs de cette compétition ces dernières années. Le solveur ManySAT est une version parallèle particulièrement efficace. C'est aussi la base de nombreux démontreurs de théorèmes et de problèmes sous forme Satisfiability Modulo Theories (SMT), qui sont des problèmes SAT dans lesquels les variables propositionnelles sont des formules d'une autre théorie mathématique. Il est étudié comme un système de preuve en complexité des preuves. L'algorithmeL'algorithme prend en entrée une formule de la logique propositionnelle en forme normale conjonctive. L'algorithme est basé sur une méthode de backtracking. Il procède en choisissant un littéral, lui affecte une valeur de vérité, simplifie la formule en conséquence, puis vérifie récursivement si la formule simplifiée est satisfaisable. Si c'est le cas, la formule originale l'est aussi, dans le cas contraire, la même vérification est faite en affectant la valeur de vérité contraire au littéral. Dans la terminologie de la littérature DPLL, c'est la conséquence d'une règle dite splitting rule (règle de séparation), et sépare le problème en deux sous problèmes. L'étape de simplification consiste essentiellement en la suppression de toutes les clauses rendues vraies par l'affectation courante, et tous les littéraux déduits faux à partir de l'ensemble des clauses restantes. DPLL étend l'algorithme de backtracking par l'utilisation des deux règles suivantes :
L'incohérence d'une affectation partielle des variables est détectée quand une clause devient vide, c'est-à-dire quand les littéraux de la clause sont tous faux. La satisfiabilité d'une formule est déterminée quand toutes les variables sont affectées sans qu'une clause ne devienne vide, ou bien, dans les implémentations modernes de l'algorithme, quand toutes les clauses sont satisfaites. L'incohérence de la formule complète ne peut être déterminée qu'après une recherche exhaustive. L'algorithme peut être décrit par le pseudo-code suivant, dans lequel Φ est une formule en forme normale conjonctive :
fonction DPLL(Φ)
si Φ est un ensemble cohérent de littéraux
alors retourner vrai;
si Φ contient une clause vide
alors retourner faux;
tant qu’il existe une clause unitaire l dans Φ
Φ ← propagation-unitaire(l, Φ);
tant qu’il existe un littéral pur l dans Φ
Φ ← affecter-littéral-pur(l, Φ);
l ← choisir-littéral(Φ);
retourner DPLL(Φ Λ l) ou DPLL(Φ Λ non(l));
avec L'algorithme de Davis–Logemann–Loveland est paramétré par le choix du littéral de branchement, c'est-à-dire la fonction Orientations ultérieuresL'efficacité et l'intérêt de DPLL ont inspiré de nombreux travaux et améliorations de l'algorithme, qui reste un sujet de recherche actif. Des travaux notables ont été effectués dans trois grandes directions : la définition d'heuristiques de branchement efficaces, la définition de nouvelles structures de données pour implémenter efficacement l'algorithme, en particulier la propagation unitaire, et enfin des extensions de l'algorithme de backtracking. Pour cette dernière direction on peut citer le backtracking non chronologique et l'apprentissage de clauses[1].
RéférencesSur le sujet
Citations
Liens externes« Démonstration pédagogique de l'algorithme DPLL », sur Institut de Recherche en Informatique et Systèmes Aléatoires |
Portal di Ensiklopedia Dunia
