Algorithme DPLL

L'algorithme de retour arrière de base consiste à choisir une valeur littérale, à lui attribuer une valeur de vérité , à simplifier la formule, puis à vérifier récursivement si la formule simplifiée est satisfaisable. Si c'est le cas, la formule originale est satisfaisable ; sinon, la même vérification récursive est effectuée en supposant la valeur de vérité opposée. C'est ce qu'on appelle la règle de division , car elle divise le problème en deux sous-problèmes plus simples. L'étape de simplification consiste essentiellement à supprimer de la formule toutes les clauses qui deviennent vraies suite à l'attribution, et toutes les valeurs littérales qui deviennent fausses dans les clauses restantes.

L'algorithme DPLL améliore l'algorithme de retour arrière par l'utilisation systématique des règles suivantes à chaque étape :

propagation unitaire

Si une clause est une clause unitaire , c'est-à-dire qu'elle ne contient qu'une seule valeur littérale non assignée, cette clause ne peut être satisfaite qu'en assignant la valeur nécessaire pour rendre cette valeur littérale vraie. Ainsi, aucun choix n'est nécessaire. La propagation unitaire consiste à supprimer toute clause contenant la valeur littérale d'une clause unitaire et à supprimer le complément de cette valeur littérale de toute clause contenant ce complément. En pratique, cela conduit souvent à des cascades déterministes d'unités, évitant ainsi une grande partie de l'espace de recherche naïf.

Élimination littérale pure

Si une variable propositionnelle n'apparaît que dans une seule polarité au sein de la formule, elle est dite pure . Une valeur littérale pure peut toujours être assignée de manière à rendre vraies toutes les clauses la contenant. Ainsi, lorsqu'elle est assignée de cette façon, ces clauses ne contraignent plus la recherche et peuvent être supprimées.

L'insatisfiabilité d'une affectation partielle est détectée lorsqu'une clause devient vide, c'est-à-dire lorsque toutes ses variables ont été initialisées de manière à rendre les littéraux correspondants faux. La satisfaisabilité de la formule est détectée soit lorsque toutes les variables sont initialisées sans générer de clause vide, soit, dans les implémentations modernes, lorsque toutes les clauses sont satisfaites. L'insatisfiabilité de la formule complète ne peut être détectée qu'après une recherche exhaustive.

L'algorithme DPLL peut être résumé dans le pseudocode suivant, où Φ est la formule CNF :

Dans ce pseudocode, `f` unit-propagate(l, Φ)et ` pure-literal-assign(l, Φ)g` sont des fonctions qui renvoient respectivement le résultat de l'application de la propagation unitaire et de la règle de la conversion littérale pure à la formule `x = 0` let à la formule ` x = 0` Φ. Autrement dit, elles remplacent chaque occurrence de `x = l0` par « vrai » et chaque occurrence de not l`x = 0` par « faux » dans la formule ` x = 0` Φ, et simplifient la formule résultante. L' opérateur ` orx` dans l' returninstruction `g` est un opérateur de court-circuitage . `x` désigne le résultat simplifié de la substitution de `x = 0` par « vrai » dans `x = 0` .Φ ∧ {l}lΦ

L'algorithme se termine dans l'un des deux cas suivants : soit la formule CNF Φest vide (c'est-à-dire qu'elle ne contient aucune clause), auquel cas elle est satisfaite par toute affectation, puisque toutes ses clauses sont trivialement vraies ; soit, lorsqu'elle contient une clause vide, cette clause est trivialement fausse, car une disjonction requiert au moins un élément vrai pour que l'ensemble soit vrai. Dans ce cas, l'existence d'une telle clause implique que la formule (évaluée comme une conjonction de toutes les clauses) ne peut pas être vraie et est donc insatisfaisable.

La fonction DPLL en pseudocode indique seulement si l'affectation finale satisfait la formule ou non. Dans une implémentation réelle, l'affectation partielle satisfaisante est généralement également renvoyée en cas de succès ; on peut la déduire en conservant la trace des littéraux de branchement et des affectations littérales effectuées lors de la propagation unitaire et de l'élimination pure des littéraux.

L'algorithme de Davis-Logemann-Loveland dépend du choix du littéral de branchement , c'est-à-dire le littéral considéré lors de l'étape de retour arrière. Par conséquent, il ne s'agit pas à proprement parler d'un algorithme, mais plutôt d'une famille d'algorithmes, un pour chaque choix possible du littéral de branchement. L'efficacité est fortement influencée par ce choix : il existe des cas où le temps d'exécution est constant ou exponentiel selon le littéral de branchement choisi. Ces fonctions de choix sont également appelées fonctions heuristiques ou heuristiques de branchement.