Algorithme DPLL

En 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. Il a été introduit en 1962 par Martin Davis, Hilary Putnam, George Logemann et . 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. Le problème SAT fait l'objet de beaucoup de recherches, et des compétitions entre solveurs sont organisées. Des implémentations modernes de DPLL comme , ou encore Minisat 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.