Propagation unitaire

La Propagation unitaire (UP pour Unit propagation) or Propagation de contrainte Booléenne ou règle du littéral unique (OLR one-literal rule) est une procédure de démonstration automatique de théorèmes utilisé pour simplifier un ensemble de clauses (en général propositionnelles).

Définition

La procédure est basée sur les clauses unitaires, c'est-à-dire. les clauses qui ne comportent qu'un unique littéral. Si un ensemble de clauses contient la clause unitaire ${\displaystyle l}$, les autres clauses sont simplifiées en appliquant les règles suivantes :

1. chaque clause (différente de l) contenant ${\displaystyle l}$ est supprimée ;
2. dans chaque clause qui contient ${\displaystyle \neg l}$ ce littéral est supprimé.

L'application de ces deux règles donne un nouvel ensemble de clause équivalent à l'original.

À titre d'exemple, l'ensemble suivant peut être simplifié par propagation unitaire parce qu'il contient la clause unitaire ${\displaystyle a}$.

${\displaystyle a\vee b}$ peut être supprimé grâce à la règle 1, elle contient le littéral ${\displaystyle a}$. Comme ${\displaystyle \neg a\vee c}$ contient la négation de a, le littéral de la clause unitaire, non a peut être supprimé de cette clause. La clause unitaire ${\displaystyle a}$ n'est pas retirée; cela rendrait l'ensemble de clause non équivalent à l'ensemble original ; elle peut cependant être retirée si elle est représentée sous une autre forme par la méthode de résolution globale (voir la section « Utilisation d'un modèle partiel »). Les effets de la méthode de résolution peuvent être représentés de la manière suivante:

${\displaystyle \{}$	${\displaystyle a\vee b,}$	${\displaystyle \neg a\vee c,}$	${\displaystyle \neg c\vee d,}$	${\displaystyle a}$	${\displaystyle \}}$
	(retiré)	(${\displaystyle \neg a}$ supprimé)	(identique)	(identique)
${\displaystyle \{}$		${\displaystyle c,}$	${\displaystyle \neg c\vee d,}$	${\displaystyle a}$	${\displaystyle \}}$

L'ensemble de clause résultant ${\displaystyle \{c,\neg c\vee d,a\}}$ est équivalent à l'original. La nouvelle clause unitaire ${\displaystyle c}$ qui résulte peut être utilisé pour une application ultérieure, qui simplifiera ${\displaystyle \neg c\vee d}$ en ${\displaystyle d}$. On peut continuer ainsi comme en propagation de contrainte jusqu'à l'obtention d'un point fixe.

Relation avec la règle de résolution

La seconde règle peut être vue comme une forme particulière de résolution, dans laquelle l'une des clauses à résoudre est tout le temps unitaire. Comme la résolution, la propagation unitaire est une règle d'inférence correcte, dans le sens où elle ne produit jamais de clauses qui ne sont déductible des autres. Les différences:

1. La résolution est une procédure de réfutation complète, tandis que la propagation unitaire ne l'est pas; c'est-à-dire que si un ensemble de clause est incohérent, la procédure de propagation unitaire peut ne pas le calculer;
2. en résolution, les clauses qui sont résolues ne peuvent pas systématiquement être supprimées de l'ensemble de clauses lors de l'ajout de la clause résultante; au contraire en propagation unitaire on peut systématiquement supprimer la clause non unitaire;
3. les procédures basées sur la résolution n'incluent pas, en général, la première règle de la propagation unitaire.

Les calculs par résolution qui incluent la subsomption peuvent modéliser la première règle par une subsomption et la seconde par une étape de résolution suivie d'une subsomption.

La propagation unitaire répétée jusqu'au point fixe est complète dans le cas où toutes les clauses sont des clauses de Horn ; elle génère aussi un ensemble minimal pour la satisfiabilité: Voir Horn-satisfiabilité.

Utiliser un modèle partiel

Les clauses unitaires incluses dans un ensemble, ou qui sont déductibles de l'ensemble, peuvent être stockées dans un «modèle partiel» (qui peut aussi contenir d'autres littéraux). Dans un tel cas, la propagation unitaire est effectuée à partir des littéraux de ce modèle, et les clauses unitaires sont retirées de l'ensemble de clauses si leur littéral est dans le modèle. Dans l'exemple, ${\displaystyle a}$ serait ajoutée au modèle partiel ; La simplification serait identique, mais a serait retiré de l'ensemble. L'ensemble en résultant est équivalent à l'original, à la condition que les littéraux du modèle partie soient valides.

Complexité

L'implantation naïve de la propagation unitaire est quadratique en fonction de la taille de l'ensemble initial, définie comme la somme de la taille de chaque clause, celle-ci étant mesurée par le nombre de littéraux qu'elle contient.

On peut cependant effectuer une passe de propagation unitaire en temps linéaire en stockant la liste de clause dans laquelle une variable apparaît, pour chaque variable. Par exemple, on numérote les clauses:

et on génère les listes suivantes :

La structure de donnée, très simple, peut être générée en temps linéaire, et permet de trouver rapidement toutes les clauses dans lesquelles une variable apparaît. La propagation unitaire peut alors itérer uniquement sur cette liste de clause. La propagation pour toutes les variables est alors linéaire en fonction du nombre de clauses.

Voir aussi

• Horn-satisfiabilité
• clause de Horn
• démonstration automatique
• algorithme DPLL
• Propagation de contraintes

Références

• (en) William Dowling et Jean Gallier, « Linear-time algorithms for testing the satisfiability of propositional Horn formulae », Journal of Logic Programming,‎ 1984, p. 267–284 (lire en ligne).
• (en) H. Zhang et M. Stickel, « An efficient algorithm for unit-propagationAn efficient algorithm for unit-propagation », Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics,‎ 1996 (lire en ligne).

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