Utilisateur:Bhoessen/Bac a sable

Problème SAT

Apprentissage de clauses provenant de conflits

Le principe des solveur de type CDCL (Constraint Driven Clause Learning) est d'utiliser un mécanisme pour apprendre de nouvelles clauses en cours de recherche, puis d'utiliser un maximum toutes les informations apprises dans l'espoir d'améliorer le temps de recherche. D'un point de vue pratique, cette méthodologie est très efficace pour résoudre des problèmes concrets. L'apprentissage de clauses est le suivant : lorsqu'un conflit apparaît lors de la recherche, c'est-à-dire lorsqu'une assignation partielle est démontrée non cohérente avec l'ensemble des clauses, on peut isoler un sous-ensemble de ces assignations et un sous-ensemble de ces clauses, qui sont responsables du conflit (les assignations ne sont pas cohérentes avec les clauses).L'apprentissage de clause permet deux choses. Premièrement, il permet d'éviter de refaire plusieurs fois les mêmes erreurs dans l'arbre de recherche. Deuxièmement, la close apprise sera en contradiction avec l'état de l'arbre de recherche. De ce fait, il sera nécessaire de réaliser un retour en arrière (backtracking) pour s'assurer qu'au moins un de ces littéral soit vrai.

Il existe différentes méthodes pour générer de nouvelles clauses à partir d'une inconsistance locale.

Méthode naïve

Soit l'instance à résoudre la formule $\phi _{1}$ suivante:

${\begin{array}{rcl}C_{1}&=&x_{1}\lor x_{2}\\C_{2}&=&\neg x_{1}\lor x_{3}\\\end{array}}$

et l'interprétation partielle ${\mathcal {I}}$ définie par: $x_{2}={\textit {faux}},x_{3}={\textit {faux}}$. Cette interprétation mène à un conflit car $x_{2}$ implique que $x_{1}=vrai$, tandis que $x_{3}$ implique que $x_{1}=faux$. Pour générer une clause représentant ce conflit, il est possible de prendre la négation de l'interprétation ${\mathcal {I}}$: $\neg {\mathcal {I}}=\neg (\neg x_{2}\land \neg x_{3})=x_{2}\lor x_{3}$. Cependant, cette méthode possède un inconvénient majeur: la clause taille de la clause est entièrement déterminée par toute l'interprétation. Or, certaines parties de l'interprétation peuvent complètement indépendante du conflit que l'on souhaite représenter. En effet, ajoutons à l'instance $\phi _{1}$ les formules: $C_{i}=x_{i}\lor x_{i+1},4\leq i\leq N$ et soit l'interprétation courante ${\mathcal {I}}=\{x_{2}=faux,x_{3}=faux,x_{4\leq i\leq N}=faux\}$. Le conflit provient des deux premières clauses et donc, des valeurs de $x_{2}$ et $x_{3}$. Or, la clause générée par la négation de l'interprétation prendra en compte toutes les variables à l'exception de x_1. De ce fait, la clause sera inutilement longue.

Analyse des conflits

Lorsque cette méthode est utilisée, un graphe est créé permettant de représenter l'origine de la propagation, appelé graphe d'implication. Les nœuds représentent les littéraux vrais. Il existe deux types de nœuds: les nœuds carrés dont la valeur du littéral provient d'un choix arbitraire et les nœuds ronds dont la valeur provient d'une propagation. À chaque nœud est également associé une information: le niveau du nœud en question. Ce niveau est défini par le nombre de littéraux choisis avant de réaliser la propagation s'il y a eu propagation. Sinon, le niveau est défini par le nombre de littéraux choisis, littéral courant compris. Les arcs relient entre eux les littéraux faisant parti d'une clause servant à la propagation. La destination d'un arc est le littéral propagé, la/les source(s) étant les autres littéraux de la clause. Soit l'instance à résoudre la formule $\phi _{2}$ suivante:

${\begin{array}{rcl}C_{1}&=&\neg d\lor f\\C_{2}&=&\neg f\lor \neg e\lor g\\C_{3}&=&\neg h\lor j\\C_{4}&=&\neg h\lor i\\C_{5}&=&\neg i\lor a\\C_{6}&=&\neg g\lor \neg i\lor b\\C_{7}&=&\neg a\lor c\\C_{8}&=&\neg b\lor \neg c\end{array}}$

accompagné de l'interprétation à laquelle les niveaux des différents littéraux ont été spécifiés ${\mathcal {I}}=\{d|_{1},f|_{1},e|_{2},g|_{2},h|_{3},i|_{3},j|_{3},a|_{3},b|_{3},c|_{3}\}$ ainsi que le littéral menant à l’inconsistance: $\neg c$. Alors, il est possible d'en tirer le graphe suivant.

Graphe d'implication

Grâce à ce graphe, il est possible de créer une clause représentant la cause du conflit. La méthode employée est la suivante: on commence par créer la résolvante ${\mathcal {R}}_{1}$ des clauses menant à un conflit. Puis tant qu'il reste plus d'un littéral du niveau courant, une nouvelle résolvante ${\mathcal {R}}_{i+1}$ est créée entre la résolvante courante ${\mathcal {R}}_{i}$ et la cause d'un des littéraux du niveau courant. Sur notre exemple, cela donnera (où $C_{i}\vdash _{\mathcal {R}}C_{j}$ représente la résolution entre la clause $C_{i}$ et la clause $C_{j}$)

${\begin{array}{rcccl}{\mathcal {R}}_{1}&=&C_{7}\vdash _{\mathcal {R}}C_{8}&=&\neg a\lor \neg b\\{\mathcal {R}}_{2}&=&{\mathcal {R}}_{1}\vdash _{\mathcal {R}}C_{6}&=&\neg g\lor \neg i\lor \neg a\\{\mathcal {R}}_{3}&=&{\mathcal {R}}_{2}\vdash _{\mathcal {R}}C_{5}&=&\neg g\lor \neg i\\{\mathcal {R}}_{4}&=&{\mathcal {R}}_{3}\vdash _{\mathcal {R}}C_{4}&=&\neg h\lor \neg g\\\end{array}}$

Retour en arrière non-chronologique

Une fois la clause apprise, celle-ci sera utilisée pour le retour en arrière. L'idée derrière le retour en arrière non-chronologique est qu'un retour en arrière sera effectué de manière à ce que l'état des assignations soit tel qu'il ne reste qu'un seul littéral non assigné. Ainsi, grâce à la clause apprise il sera possible de continuer les différentes propagations alors que cela n'était plus possible sans elle.

Si l'on reprend l'exemple $\phi _{2}$ présenté dans la section analyse de conflit, la clause apprise ${\mathcal {R}}_{4}=\neg h\lor \neg g$ nous procure deux littéraux. Les niveaux des variables correspondantes sont: variable $h$ = 3, variable $g$ = 2. Pour savoir à quel niveau il est nécessaire de revenir en arrière, il faut regarder le niveau le plus profond (le niveau $i+1$ est plus profond que le niveau $i$) des variables d'un niveau plus haut que le niveau actuel. Étant donné que la clause apprise ne contient que deux littéraux, il n'existe qu'un seul niveau différent du niveau actuel: le niveau 2. Un retour en arrière est donc effectué jusqu'à ce niveau et laisse donc comme interprétation ${\mathcal {I}}=\{d|_{1},f|_{1},e|_{2},g|_{2}\}$. Or, avec une telle interprétation, la clause apprise ne contient bien qu'une seule variable non affectée: $h$ tandis que l'autre est affectée de telle manière à ce que le littéral $\neg g$ soit faux. Cela implique la nécessité d'une propagation de la variable $h$ à la valeur faux.

Bien que dans cet exemple le retour en arrière ne s'effectue que sur un seul niveau, il est possible que celui-ci monte de plusieurs niveau d'un coup. En effet, imaginons que nous puissions ajouter N niveaux entre le niveau 2 et le niveau 3 où toutes les variables qui y apparaissent soient de nouvelles variables. Puisque ces niveaux n'auraient pas d'impact sur l'ancien niveau 3, le retour en arrière remonterait d'un coup ces N+1 niveaux.