Algorithme DPLL

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

L'algorithme de Davis–Putnam–Logemann–Loveland (DPLL) est un algorithme de backtracking, complet, de résolution du problème SAT exprimé en forme normale conjonctive. Il 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].

Ce problème est très important en théorie de la complexité et a de nombreuses applications en planification classique, model checking, diagnostic, et jusqu'au configurateur d'un PC ou de son système d'exploitation.

Implémentations et applications[modifier | modifier le code]

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 par exemple.

À ce titre, il fait l'objet de beaucoup de recherches, et des compétitions entre solveurs[2] sont organisées. Des implantations 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.

L'algorithme[modifier | modifier le code]

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ème.

L'étape de simplification consiste essentiellement en la suppression de toutes les clauses rendue 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 :

La propagation unitaire 
Si une clause est unitaire, c'est-à-dire qu'elle contient un et un seul littéral, elle ne peut être satisfaite qu'en affectant l'unique valeur qui la rend vraie à son littéral. Il n'y a par conséquent plus à choisir. En pratique, son application entraîne une cascade d'autres clauses unitaires de manière déterministe, et évite donc d'explorer une grande part de l'espace de recherche. Elle peut être vue comme une forme de propagation de contraintes.
L'élimination des littéraux dits purs 
Si une variable propositionnelle apparaît seulement sous une forme (soit seulement positive, soit seulement négative) ses littéraux sont dits purs. Les littéraux purs peuvent être affectés d'une manière qui rend toutes les clauses qui les contiennent vrais. Par conséquents ces clauses ne contraignent plus l'espace de recherche et peuvent être éliminées.

L'incohérence d'une affectation partielle des variables est détectée quand une clause devient vide, c'est-à-dire quand toutes ses variables sont affectées de manière à ce que les littéraux correspondants soient 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 implantations 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 dans le pseudocode suivant, dans lequel Φ est la 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;
   pour chaque clause unitaire l dans Φ
       Φ=propagation-unitaire(l, Φ);
   pour chaque littéral-pur l dans Φ
       Φ=affecter-littéral-pur(l, Φ);
   l := choisir-littéral(Φ);
   retourner DPLL(ΦΛl) ou DPLL(ΦΛnon(l));

avec propagation-unitaire(l, Φ) et affecter-littéral-pur(l, Φ) définis comme des fonctions qui calculent et retournent le résultat de l'application de la règle respectivement de propagation unitaire et de la règle de littéral pur, à partir d'un littéral l et d'une formule Φ. En d'autres termes, elles remplacent chaque occurrence de l par vrai, chaque occurrence de non(l) par faux dans Φ, et simplifient la formule résultante. Ce pseudocode ne fait que retourner le résultat du problème de décision, une implantation réelle retournerait aussi typiquement une affectation partielle qui rend la formule vraie. Cette affectation peut être déduite à partir de l'ensemble de littéraux cohérent du premier si de la fonction.

L'algorithme de Davis–Logemann–Loveland est paramétré par le choix du littéral de branchement, c'est-à-dire la fonction choisir-littéral dans le pseudocode, le littéral choisi pour l'étape de backtracking. Ce n'est donc pas un algorithme à proprement parler mais toute une famille d'algorithmes, un pour chaque choix de fonction choisir-littéral possible. On parle aussi d'heuristique de branchement[6]. Ce choix influe drastiquement sur l'efficacité de l'algorithme: il peut exister des instances de SAT pour lequel le temps d'exécution est constant pour certaines heuristiques de branchement et exponentiel pour d'autres.

Orientation ultérieures[modifier | modifier le code]

L'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 implanter efficacement l'algorithme, en particulier la propagation unitaire, et enfin des extension de l'algorithme de backtracking. Pour cette dernière direction on peut citer le backtracking non chronologique et l'apprentissage de clauses[1].

Le backtracking non-chronologique

(ou backjumping (en) ) consiste en l'inférence d'une clause dite de conflit (conflict clause) qui résume les racines d'un conflit, c'est-à-dire l'affectation de certaines variables qui conduisent inévitablement à un échec. Il devient possible de revenir à une décision plus ancienne que la dernière décision (la première décision qui n'implique pas que la clause de conflit soit nécessairement vraie).

L'apprentissage.

La clause de conflit inférée lors du backjumping peut être ajoutée à l'ensemble des clauses pour éviter que la recherche ne conduise ultérieurement à une situation identique.

Références[modifier | modifier le code]

Sur le sujet

Citations

  1. a et b Robert Nieuwenhuis, Albert Oliveras et Cesar Tinelly, « Abstract DPLL and Abstract DPLL Modulo Theories », Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2004, Proceedings,‎ 2004, p. 36-50 (lire en ligne)
  2. « site de compétition de solveur SAT »
  3. « site web de zchaff »
  4. « Site de chaff »
  5. « Site de minisat »
  6. João Marques-silva, « The impact of branching heuristics in propositional satisfiability algorithms », In 9th Portuguese Conference on Artificial Intelligence (EPIA),‎ 1999 (DOI 10.1.1.111.9184, lire en ligne)