Une procédure de recherche récursive par retour arrière pour la satisfaisabilité propositionnelle qui combine la séparation de variables, la propagation d'unités (propagation des contraintes booléennes), l'élimination des littéraux purs et le retour arrière systématique pour décider si une formule en CNF est satisfiable.

Principe

Réduire la recherche en déduisant des affectations forcées (propagation d'unités) et en éliminant les choix évidents (littéraux purs), séparer sur des variables seulement quand nécessaire, et revenir en arrière en cas de contradictions pour explorer un arbre de recherche exponentiel mais prunable.

Démonstration

Pour décider la satisfiabilité de (A ∨ B) ∧ (¬A ∨ C) ∧ (¬B ∨ ¬C), l'algorithme applique la propagation d'unités quand des clauses unitaires apparaissent, choisit un littéral de branchement (par exemple A), explore récursivement A = vrai puis A = faux, et revient en arrière si une contradiction survient jusqu'à trouver une affectation satisfaisante ou prouver l'insatisfaisabilité.

Mauvaise application

Considérer DPLL comme une recherche purement gloutonne sans maintenir ni appliquer la propagation d'unités ou l'apprentissage de clauses conduit à des explorations redondantes et à une dégradation sévère des performances sur de nombreux problèmes SAT.

Conséquence

Bien appliqué, DPLL peut décider efficacement de nombreux cas SAT pratiques en élaguant de larges portions de l'espace de recherche ; il constitue la base des solveurs SAT modernes et permet des améliorations pilotées par les conflits.

Inversion

Inverser le concept en effectuant une énumération exhaustive aveugle de toutes les affectations sans propagation ni heuristiques de retour arrière ; cela conserve la correction mais perd l'élagage et l'exploitation de la structure nécessaires à l'échelle.

Limite

S'applique à la logique propositionnelle en CNF et aux procédures de décision centrées sur la structure booléenne ; il ne gère pas à lui seul des théories avec fonctions interprétées (SMT) sans être combiné à un raisonnement spécifique à la théorie.

Tension sémantique

Entre en tension avec des procédures purement résolutives ou algébriques : la résolution dérive globalement des conséquences par combinaison de clauses, tandis que DPLL met l'accent sur la recherche avec propagation locale et décisions de branchement.

Synthèse

DPLL combine la déduction logique locale (propagation d'unités et élimination des littéraux purs) avec une recherche systématique et le retour arrière pour transformer la résolution SAT en une exploration contrôlable d'un arbre d'affectations prunable, formant l'ossature algorithmique des procédés propositionnels modernes.