Le mécanisme algorithmique qui assigne itérativement les valeurs impliquées par les clauses unitaires dans un ensemble de clauses propositionnelles afin de simplifier l'instance et de détecter des conflits ; couramment appelé propagation de contraintes booléennes (BCP).

Principe

Si une clause devient unitaire (un seul littéral non attribué), ce littéral doit être mis vrai pour satisfaire la clause ; propager cette assignation dans l'ensemble de clauses, simplifier les clauses et répéter jusqu'à point fixe ou conflit.

Démonstration

Pour les clauses { {p}, {¬p, q}, {¬q} }, propager p=true à partir de {p} ; cela satisfait {¬p, q} qui peut être supprimée, laissant {¬q} qui force q=false ; la suite de propagations unitaires simplifie l'instance et révèle cohérence ou conflit.

Mauvaise application

Appliquer la propagation unitaire à des formules qui n'ont pas été réduites en forme de clauses sans tenir compte de la structure introduite, ou supposer que la propagation préserve d'autres propriétés comme la portée des quantificateurs ou des contraintes spécifiques à une théorie.

Conséquence

La propagation unitaire réduit rapidement l'espace de recherche, détecte tôt les contradictions et constitue une inférence peu coûteuse essentielle qui sous-tend la résolution efficace SAT et l'élagage dans les cadres DPLL/CDCL.

Inversion

Omettre la propagation et ne faire que des branches sur les variables force une exploration combinatoire des assignations que la propagation unitaire aurait élaguée, augmentant typiquement la recherche de manière exponentielle.

Limite

Définie pour des ensembles de clauses propositonnelles en CNF ; les extensions à des théories plus riches nécessitent une propagation spécifique à la théorie (par ex. congruence, arithmétique linéaire), et la propagation doit être implémentée avec soin pour rester correcte.

Tension sémantique

La propagation unitaire est souvent confondue avec la propagation de contraintes générale ou la simplification booléenne complète ; c'est une inférence syntaxique étroite fondée sur les unités dont la puissance dépend de la structure des clauses et des structures de données du solveur (littéraux surveillés).

Synthèse

La propagation unitaire est le processus déterministe itératif d'affectation et de propagation de littéraux forcés issus de clauses unitaires pour simplifier les clauses et détecter des conflits, formant l'inférence légère de base des procédures SAT modernes.