Satisfaisabilité, frustration et transitions de phase

11 janvier 2025 — Rust, Informatique théorique, Physique

Vous êtes chargé des invitations pour une grande fête familiale, mais vos proches vous ont imposé certaines conditions :

• Votre mère vous demande d’inviter Pierre, ou de ne pas inviter Romane.
• Votre frère vous demande d’inviter Romane ou Quentin (ou les deux).
• Votre oncle, lui, veut snober soit Quentin soit Pierre (soit les deux).

Question : Existe-t-il une liste d’invités qui satisfasse toutes ces clauses ?

Les conditions énoncées dans le petit problème présenté ci-dessus peuvent se résumer dans la formule logique suivante :

$(\text{Pierre} \lor \lnot \text{Romane}) \land (\text{Romane} \lor \text{Quentin}) \land (\lnot \text{Quentin} \lor \lnot \text{Pierre})$

Il se trouve que cette formule est satisfaisable, par exemple en invitant Pierre et Romane, mais en excluant Quentin.

Intuitivement, on peut imaginer que plus on ajoute de clauses à une formule, moins elle a de chances d’être satisfaisable.

Dans cet article, nous allons vérifier expérimentalement cette intuition et mettre en évidence un phénomène de transition de phase entre un régime de satisfaisabilité et un régime de non-satisfaisabilité des formules, lorsque le nombre de clauses augmente.

Nous verrons dans un second temps comment ce problème peut se traduire en termes énergétiques, par analogie avec certains modèles physiques.

Quelques mots sur la satisfaisabilité

Le problème de satisfaisabilité booléenne (SAT) s’intéresse à des formules constituées à l’aide des opérateurs logiques $\lor$ (ou), $\land$ (et), $\lnot$ (non).

Les propriétés de ces opérateurs logiques permettent de transformer toute formule ainsi formée en une formule équivalente sous forme normale conjonctive (CNF), comme celle présentée en introduction :

Cette formule est constituée d’une conjonction ($\land$) de clauses, chacune de ces clauses étant constituée d’une disjonction ($\lor$) de littéraux (une variable ou sa négation).

Le problème de la satisfaisabilité consiste à se demander si l’on peut attribuer à chaque variable intervenant dans la formule une valeur de vérité de façon à ce que la formule soit vérifiée.

Dans ce cas c’est possible, par exemple avec les assignations suivantes :

Algorithmes de résolution

Le problème de déterminer, pour une formule booléenne quelconque, si elle est satisfaisable, s’appelle le problème SAT.

Le problème k-SAT consiste à déterminer la satisfaisabilité d’une formule sous forme normale conjonctive dont les clauses sont toutes de taille $k$. Par exemple, la formule présentée précédemment correspond à $k = 2$ : ses clauses sont toutes composées de deux littéraux.

Les problèmes SAT et k-SAT ($k \geq 3$) sont des problèmes NP-complet, mais on peut les résoudre en un temps raisonnable dans beaucoup de cas grâce à des algorithmes de backtracking.

💡 Le cas de 2-SAT

Le problème 2-SAT peut se résoudre en temps polynomial.

L’algorithme implémenté ici consiste, par exemple, à remarquer qu’une clause comme $A \lor B$ est équivalente aux implications $\lnot A \Rightarrow B$ et $\lnot B \Rightarrow A$.

On construit alors un graphe orienté dont les sommets correspondent aux littéraux (e.g. $\lnot A, B, ...$) et les arêtes aux implications associées aux clauses de la formule. Deux littéraux sont alors dans la même composante fortement connexe du graphe si et seulement si on peut passer de l’un à l’autre et réciproquement via une chaîne d’implications.

Si, pour une variable $x$, les littéraux $x$ et $\lnot x$ sont dans la même composante, cela signifie que la formule est contradictoire. En fait — et ce n’est pas complètement immédiat — cela donne un ensemble de conditions nécessaires et suffisantes pour obtenir la satisfaisabilité.

On pourra lire le chapitre consacré du livre Introduction to Algorithms pour plus de détails.

Étude de la transition satisfaisabilité → frustration

I can’t get no satisfaction
‘Cause I try and I try and I try and I try
— The Rolling Stones

Le programme satisfaction, que j’ai écrit en Rust, permet d’étudier la satisfaisabilité d’instances aléatoires du problème k-SAT lorsque le nombre de clauses augmente.

Plus précisément, considérons le nombre $\alpha = \cfrac{\text{Nombre de clauses}}{N}$, où $N$ désigne le nombre de variables sur lesquelles porte la formule.

Dans le cas d’introduction, on a par exemple $\alpha = 1$ puisque l’on a trois clauses et trois variables.

Étudions le pourcentage d’instances satisfaisables sur un échantillon aléatoire lorsque $\alpha$ varie.

Problème 2-SAT

Voici ce que l’on obtient pour des formules de taille 2 portant sur 10 variables (l’indication s.p.p correspond au nombre de formules aléatoires générées pour chaque point) :

Le taux de formules satisfaisables diminue avec $\alpha$ (on s’y attendait), selon une courbe plutôt lisse.

Pour des formules portant sur 1000 variables, l’évolution est beaucoup plus abrupte :

On distingue deux régimes que je nommerai satisfaisabilité et frustration (ce nom sera justifié en dernière partie) :

• Satisfaisabilité : à gauche ($\alpha$ petit), les formules sont presque toutes satisfaisables
• Frustration : à droite ($\alpha$ grand), les formules sont presque toutes non-satisfaisables

Dans le cas limite $N \to +\infty$, ces deux régimes sont séparés strictement par la valeur $\alpha_C = 1$.

💡 Dans le cas de 2-SAT, il est possible de démontrer l’existence de cette transition et la valeur de $\alpha_C$. On pourra consulter ce papier pour une preuve, ainsi que celui-ci qui précise le comportement asymptotique.

Problème 3-SAT

Les simulations dans le cas de 3-SAT sont plus lourdes à générer, le problème étant NP-complet.

Pour des valeurs de $N$ raisonnables, on peut néanmoins observer aussi une transition de phase. Dans ce cas, on estime qu’elle se situe autour de $\alpha_C \approx 4.3$, mais on a moins de résultats théoriques que pour 2-SAT.

On pourra également consulter le papier Phase transitions and complexity in computer science: an overview qui présente des résultats pour des formules hybrides, comportant des clauses de tailles 2 et 3.

Une approche énergétique de la satisfaisabilité

Considérons à nouveau la formule présentée en introduction : ${(\text{Pierre} \lor \lnot \text{Romane}) \land (\text{Romane} \lor \text{Quentin}) \land (\lnot \text{Quentin} \lor \lnot \text{Pierre})}$.

Représentons les grandeurs booléennes $i = P, Q, R$ ($\text{Pierre}, \text{Quentin}, \text{Romane}$) par des variable $\sigma_i \in \{ 1, -1 \}$ (avec $1 = \text{Vrai}$, $-1 = \text{Faux}$).

Dès lors, on peut associer à la formule une fonction « énergie » :

$E = \frac{1}{4} [(1 - \sigma_{P})(1 + \sigma_{R}) + (1 - \sigma_{R})(1 - \sigma_{Q}) + (1 + \sigma_{Q})(1 + \sigma_{P})]$

Ainsi définie, je vous laisse vous convaincre que $E$ correspond, pour chaque assignation des variables, au nombre de clauses non satisfaites dans la formule.

La satisfaisabilité se traduit alors par la condition que l’énergie minimale accessible soit égale à $0$.

En développant le calcul on obtient $E = - \frac{1}{4} (\sigma_{P}\sigma_{R} - \sigma_{Q}\sigma_{R} - \sigma_{P}\sigma_{Q} - 3)$.

Cette quantité s’annule lorsque $\sigma_{P}$ et $\sigma_{R}$ sont de même signe et $\sigma_{Q}$ de signe opposé : on retrouve la solution proposée en introduction, ainsi que l’alternative correspondant à exclure Pierre et Romane et inviter Quentin.

Lien avec le modèle d’Ising

Plus généralement, une formule 2-SAT va correspondre à une énergie ${E = - \sum_{i,j} J_{ij} \sigma_i \sigma_j - \sum_{i} h_i \sigma_i + \lambda}$.

C’est la forme générale de l’énergie du modèle d’Ising, les $(J_{ij})$ et $(h_i)$ étant des constantes de couplage.

Le cas le plus classique d’application du modèle d’Ising est la modélisation des propriétés magnétiques de certains matériaux.

Généralement, on considère que le matériau est consitué d’un réseau de petits aimants qui interagissent, chacun avec ses plus proches voisins, selon un terme de couplage constant $J$.

En l’absence de champ magnétique extérieur, l’énergie s’exprime alors simplement ${E = - \sum_{(i,j) \text{voisins}} J \sigma_i \sigma_j}$.

À basse température, le système va s’arranger de façon à minimiser cette énergie, ce qui conduit à différents comportements selon le couplage.

Dans le cas $J > 0$ (ferromagnétisme), les aimants tendent à s’aligner (cliquer sur la grille pour alterner entre les deux variantes) :

Dans le cas $J \lt 0$ (antiferromagnétisme), les aimants tendent à s’opposer à leurs voisins :

Dans les deux cas illustrés ci-dessus, comme dans l’exemple d’introduction, les fonctions d’énergie correspondent à des formules satisfaisables : lorsque l’énergie (totale) est minimale, elle l’est aussi pour chaque terme d’interaction isolé.

Non-satisfaisabilité et frustration magnétique

Considérons la formule suivante :

$(\lnot A \lor \lnot B) \land (A \lor B) \land (\lnot B \lor \lnot C) \land (B \lor C) \land (\lnot C \lor \lnot A) \land (C \lor A)$

En développant la fonction d’énergie associée à cette formule, on obtient :

Cette énergie est celle associée à une configuration triangulaire du modèle d’Ising, avec un terme d’interaction antiferromagnétique ($J \lt 0$) :

Comme illustré ci-dessus (cliquer sur le triangle !), il y a six configurations qui minimisent l’énergie de ce système, mais dans chacune d’entre elles au moins deux aimants voisins sont alignés : le système est frustré.

Cette frustration correspond exactement à la non-satisfaisabilité de la formule correspondante.

La vidéo ci-dessous (du centre de recherche ct.qmat) montre une manifestation grandeur nature de la frustration magnétique dans un réseau d’aimants arrangés selon un pavage de Kagomé.

Les systèmes frustrés présentent généralement une multitude d’états d’énergie minimale, ce qui donne lieu à différents phénomènes qui peuvent intéresser les physiciens. Pour approfondir, on pourra lire cette introduction à la physique des systèmes frustrés, par Leticia Cugliandolo.

Maths et applications, avec les mains et avec du code 💻
Suivre sur Twitter

• ← Quelques aspects de la mécanisation de la géométrie