Algorithme DPLL

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].

Le 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'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 :

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 partie 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 forme positive ou seulement sous forme négative alors 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équent 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 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 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 implémentation 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 pseudo-code, 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 classes d'instances de SAT pour lequel le temps d'exécution est constant pour certaines heuristiques de branchement et exponentiel pour d'autres.

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 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].

Le backtracking non-chronologique

(ou backjumping ) 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.

Sur le sujet

• (en) Martin Davis, « A Computing Procedure for Quantification Theory », Journal of the ACM, vol. 7, n^o 3,‎ 1960, p. 201–215 (DOI 10.1145/321033.321034, lire en ligne).
• (en) Martin Davis, « A Machine Program for Theorem Proving », Communications of the ACM, vol. 5, n^o 7,‎ 1962, p. 394–397 (DOI 10.1145/368273.368557, lire en ligne).
• (en) Ming Ouyang, « How Good Are Branching Rules in DPLL? », Discrete Applied Mathematics, vol. 89, n^os 1–3,‎ 1998, p. 281–286 (DOI 10.1016/S0166-218X(98)00045-6).
• (en) John Harrison, Handbook of practical logic and automated reasoning, Cambridge University Press, 2009 [détail des éditions] (ISBN 9780521899574), p. 79-90.

Citations

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « DPLL algorithm » (voir la liste des auteurs).

« Démonstration pédagogique de l'algorithme DPLL », sur Institut de Recherche en Informatique et Systèmes Aléatoires

• Portail de l'informatique théorique