Navigation : Index Z3 | Index SymbolicAI | Index général | << 11 Job Shop Scheduling
χ(G) — le plus petit nombre de couleurs nécessaire — par recherche linéaire (suite de requêtes SAT)Durée estimée : 35-45 minutes
La coloration de graphe est un problème NP-difficile classique : étant donné un graphe, attribuer une couleur à chaque sommet de sorte que deux sommets reliés par une arête aient des couleurs différentes, en minimisant le nombre de couleurs. Ses applications sont nombreuses : planification d’examens (sommet = examen, arête = étudiant commun, couleur = créneau horaire), allocation de registres dans un compilateur, attribution de fréquences radio, etc.
Ce notebook le démontre sur le graphe de Petersen, un graphe à 10 sommets et 15 arêtes, célèbre parce qu’il sert de contre-exemple à de nombreuses conjectures. Son nombre chromatique vaut χ = 3 — mais une lecture naïve pourrait en suggérer davantage, et une heuristique gloutonne s’y trompe. C’est exactement le terrain où le solveur fait la différence.
flowchart LR
G["Graphe de Petersen\n(10 sommets, 15 aretes)"]
G --> GR["Heuristique gloutonne\nfirst-fit (ordre 0..9)"]
G --> Z["Modèle Z3.Linq\n1 couleur par sommet\nCi != Cj sur chaque arete"]
GR --> KG["3 ou 4 couleurs\nselon l'ordre de parcours\n(aucune garantie)"]
Z --> RL["Recherche lineaire\nk = 1, 2, 3, ...\npremier SAT = chi(G)"]
RL --> CHI["chi(G) = 3\n(optimum PROUVE,\n2 couleurs = UNSAT)"]
KG --> C["Comparaison"]
CHI --> C
%% color: explicite -- sans lui, libelle clair sur fond clair en mode sombre GitHub (#15022) ; ton parfois plus fonce que le stroke (le stroke en couleur de texte rendrait infer illisible) : ne pas harmoniser
style CHI fill:#c8f7c5,color:#1b5e20
style KG fill:#f7d5c5,color:#8a3e1eLes deux voies partent du même graphe. Le glouton colore les sommets dans l’ordre, sans anticiper : selon l’ordre, il trouve 3 couleurs (chanceux) ou 4 (malchanceux), sans jamais le savoir. Le solveur explore globalement l’espace des colorations, atteint χ = 3 et le prouve (il démontre que 2 couleurs sont impossibles). Le payoff pédagogique : non pas « le glouton se trompe toujours », mais « le glouton ne garantit ni l’optimum ni la preuve », là où Z3 fait les deux.
#r "../Z3.Linq/.deploy/Microsoft.Z3.dll"
#r "../Z3.Linq/.deploy/ExpressionUtils.dll"
#r "../Z3.Linq/.deploy/Z3.Linq.dll"
using Z3.Linq;
using Microsoft.Z3;
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
Console.WriteLine("Imports OK : Z3.Linq (.deploy), Microsoft.Z3, System.Linq");Imports OK : Z3.Linq (.deploy), Microsoft.Z3, System.LinqLe graphe de Petersen se construit ainsi : - un pentagone externe : les sommets 0-1-2-3-4 reliés en cycle ; - un pentagramme interne : les sommets 5-6-7-8-9 reliés en étoile (5-7-9-6-8-5) ; - cinq rayons reliant chaque sommet externe i au sommet interne i+5.
Soit 15 arêtes au total. Ci-dessous, on encode la liste d’adjacence et un utilitaire d’affichage d’une coloration.
// Graphe de Petersen : 10 sommets (0..9), 15 aretes
int N = 10;
var edges = new List<(int, int)>
{
// Pentagone externe
(0,1),(1,2),(2,3),(3,4),(4,0),
// Rayons externe -> interne
(0,5),(1,6),(2,7),(3,8),(4,9),
// Pentagramme interne
(5,7),(7,9),(9,6),(6,8),(8,5)
};
// Liste d'adjacence (pour le glouton)
var adj = Enumerable.Range(0, N).ToDictionary(v => v, v => new List<int>());
foreach (var (a, b) in edges) { adj[a].Add(b); adj[b].Add(a); }
void DisplayColoring(int[] color, string title)
{
Console.WriteLine(title);
int k = color.Max() + 1;
Console.WriteLine($" Couleurs utilisees : {k}");
for (int v = 0; v < color.Length; v++)
Console.WriteLine($" Sommet {v} -> couleur {color[v]}");
// Verification : aucune arete monochrome
bool valid = edges.All(e => color[e.Item1] != color[e.Item2]);
Console.WriteLine($" Coloration valide (aucune arete monochrome) : {valid}");
}
Console.WriteLine($"Graphe de Petersen charge : {N} sommets, {edges.Count} aretes.");Graphe de Petersen charge : 10 sommets, 15 aretes.L’algorithme first-fit parcourt les sommets dans un ordre donné et attribue à chacun la plus petite couleur non encore utilisée par ses voisins déjà colorés. Simple et rapide, mais myope : il ne revient jamais sur une décision, et son résultat dépend de l’ordre de parcours.
Pour le montrer, on le lance deux fois sur le même graphe : une fois dans l’ordre naturel 0..9, une fois dans un ordre défavorable. Le degré maximal du graphe de Petersen étant 3, first-fit peut utiliser jusqu’à Δ + 1 = 4 couleurs.
// Coloration gloutonne first-fit selon un ordre de parcours donne
int[] GreedyColoring(int n, Dictionary<int, List<int>> adjacency, int[] order)
{
var color = Enumerable.Repeat(-1, n).ToArray();
foreach (int v in order)
{
var used = new HashSet<int>();
foreach (int w in adjacency[v])
if (color[w] != -1) used.Add(color[w]);
int c = 0;
while (used.Contains(c)) c++;
color[v] = c;
}
return color;
}
// Ordre naturel 0..9
int[] naturalOrder = Enumerable.Range(0, N).ToArray();
int[] greedyNatural = GreedyColoring(N, adj, naturalOrder);
int greedyNaturalColors = greedyNatural.Max() + 1;
DisplayColoring(greedyNatural, "First-fit, ordre naturel 0..9 :");
Console.WriteLine();
// Ordre defavorable (force la 4e couleur)
int[] badOrder = { 4, 8, 2, 6, 5, 9, 0, 7, 1, 3 };
int[] greedyBad = GreedyColoring(N, adj, badOrder);
int greedyBadColors = greedyBad.Max() + 1;
DisplayColoring(greedyBad, "First-fit, ordre defavorable {4,8,2,6,5,9,0,7,1,3} :");
Console.WriteLine();
Console.WriteLine($"Meme graphe, meme algorithme : {greedyNaturalColors} couleurs vs {greedyBadColors} couleurs selon l'ordre.");First-fit, ordre naturel 0..9 :
Couleurs utilisees : 3
Sommet 0 -> couleur 0
Sommet 1 -> couleur 1
Sommet 2 -> couleur 0
Sommet 3 -> couleur 1
Sommet 4 -> couleur 2
Sommet 5 -> couleur 1
Sommet 6 -> couleur 0
Sommet 7 -> couleur 2
Sommet 8 -> couleur 2
Sommet 9 -> couleur 1
Coloration valide (aucune arete monochrome) : True
First-fit, ordre defavorable {4,8,2,6,5,9,0,7,1,3} :
Couleurs utilisees : 4
Sommet 0 -> couleur 2
Sommet 1 -> couleur 3
Sommet 2 -> couleur 0
Sommet 3 -> couleur 1
Sommet 4 -> couleur 0
Sommet 5 -> couleur 1
Sommet 6 -> couleur 1
Sommet 7 -> couleur 3
Sommet 8 -> couleur 0
Sommet 9 -> couleur 2
Coloration valide (aucune arete monochrome) : True
Meme graphe, meme algorithme : 3 couleurs vs 4 couleurs selon l'ordre.Les deux exécutions le montrent : sur le même graphe, first-fit donne 3 couleurs dans l’ordre naturel mais 4 dans l’ordre défavorable. Le glouton produit toujours une coloration valide, mais le nombre de couleurs dépend de l’ordre et n’est pas garanti minimal. Pire : le glouton n’a aucun moyen de savoir si l’ordre qu’il a suivi était bon — il ne peut ni prouver qu’il est optimal, ni qu’un autre ordre ferait mieux. C’est la limite structurelle des heuristiques sans retour arrière.
La question devient alors : combien de couleurs sont réellement nécessaires ? C’est le nombre chromatique χ(G), et c’est précisément ce qu’un solveur SMT sait établir — avec une preuve.
On déclare une classe modèle avec une variable entière par sommet (C0 à C9), représentant sa couleur. Pour un nombre de couleurs k fixé, les contraintes sont :
Ci est dans [0, k) ;(i, j), Ci ≠ Cj. On l’exprime sous forme disjonctive (Ci < Cj || Ci > Cj), qui n’utilise que des opérateurs déjà éprouvés du binding ;C0 = 0, puisque le nom des couleurs est arbitraire.En faisant croître k (1, 2, 3, …), la première valeur pour laquelle le théorème est satisfiable est le nombre chromatique.
// Modele Z3 : une couleur entiere par sommet du graphe de Petersen
public class GraphColoring
{
public int C0 = 0;
public int C1 = 0;
public int C2 = 0;
public int C3 = 0;
public int C4 = 0;
public int C5 = 0;
public int C6 = 0;
public int C7 = 0;
public int C8 = 0;
public int C9 = 0;
}
Console.WriteLine("Classe modele GraphColoring definie (10 variables de couleur).");Classe modele GraphColoring definie (10 variables de couleur).On enchaîne les requêtes SAT pour k = 1, 2, 3, …. Pour chaque k, on construit un théorème dont les contraintes de domaine bornent les couleurs à [0, k) et dont chaque arête interdit l’égalité des deux extrémités. La première valeur de k satisfiable donne χ(G) et une coloration témoin.
// Recherche lineaire du nombre chromatique
GraphColoring optimal = null;
int chromatic = -1;
for (int k = 1; k <= N; k++)
{
int kk = k; // capture locale
using (var ctx = new Z3Context())
{
var theorem = ctx.NewTheorem<GraphColoring>()
// 1. Domaine : chaque couleur dans [0, k)
.Where(t => t.C0 >= 0 && t.C0 < kk && t.C1 >= 0 && t.C1 < kk
&& t.C2 >= 0 && t.C2 < kk && t.C3 >= 0 && t.C3 < kk
&& t.C4 >= 0 && t.C4 < kk && t.C5 >= 0 && t.C5 < kk
&& t.C6 >= 0 && t.C6 < kk && t.C7 >= 0 && t.C7 < kk
&& t.C8 >= 0 && t.C8 < kk && t.C9 >= 0 && t.C9 < kk)
// 2. Brisure de symetrie : la couleur du sommet 0 est fixee
.Where(t => t.C0 == 0)
// 3. Aretes : extremites de couleurs differentes (forme disjonctive)
// Pentagone externe
.Where(t => t.C0 < t.C1 || t.C0 > t.C1)
.Where(t => t.C1 < t.C2 || t.C1 > t.C2)
.Where(t => t.C2 < t.C3 || t.C2 > t.C3)
.Where(t => t.C3 < t.C4 || t.C3 > t.C4)
.Where(t => t.C4 < t.C0 || t.C4 > t.C0)
// Rayons
.Where(t => t.C0 < t.C5 || t.C0 > t.C5)
.Where(t => t.C1 < t.C6 || t.C1 > t.C6)
.Where(t => t.C2 < t.C7 || t.C2 > t.C7)
.Where(t => t.C3 < t.C8 || t.C3 > t.C8)
.Where(t => t.C4 < t.C9 || t.C4 > t.C9)
// Pentagramme interne
.Where(t => t.C5 < t.C7 || t.C5 > t.C7)
.Where(t => t.C7 < t.C9 || t.C7 > t.C9)
.Where(t => t.C9 < t.C6 || t.C9 > t.C6)
.Where(t => t.C6 < t.C8 || t.C6 > t.C8)
.Where(t => t.C8 < t.C5 || t.C8 > t.C5);
var sol = theorem.Solve();
if (sol != null)
{
optimal = sol;
chromatic = kk;
Console.WriteLine($"k = {kk} -> SAT : nombre chromatique trouve !");
break;
}
else
{
Console.WriteLine($"k = {kk} -> UNSAT (impossible avec {kk} couleur(s))");
}
}
}
Console.WriteLine();
Console.WriteLine($"Nombre chromatique chi(Petersen) = {chromatic}");k = 1 -> UNSAT (impossible avec 1 couleur(s))
k = 2 -> UNSAT (impossible avec 2 couleur(s))
k = 3 -> SAT : nombre chromatique trouve !
Nombre chromatique chi(Petersen) = 3χ = 3 prouvéLa recherche établit que le graphe de Petersen n’est pas 2-coloriable (UNSAT pour k = 2 — il contient des cycles impairs) mais l’est avec 3 couleurs (SAT pour k = 3). C’est un résultat prouvé, pas estimé : pour k = 2, le solveur a démontré qu’aucune assignation ne satisfait toutes les arêtes ; pour k = 3, il exhibe une coloration témoin.
L’écart avec le glouton est le cœur du propos : là où l’heuristique gaspille une couleur, le solveur atteint et certifie l’optimum.
// Extraction et verification de la coloration optimale
int[] z3color = {
optimal.C0, optimal.C1, optimal.C2, optimal.C3, optimal.C4,
optimal.C5, optimal.C6, optimal.C7, optimal.C8, optimal.C9
};
DisplayColoring(z3color, $"Coloration optimale Z3 (chi = {chromatic}) :");
Console.WriteLine();
Console.WriteLine("=== Comparaison ===");
Console.WriteLine($" Glouton first-fit (ordre naturel) : {greedyNaturalColors} couleurs");
Console.WriteLine($" Glouton first-fit (ordre defavorable): {greedyBadColors} couleurs");
Console.WriteLine($" Z3 (optimum PROUVE) : {chromatic} couleurs");
Console.WriteLine($" Dans le pire ordre, le glouton gaspille {greedyBadColors - chromatic} couleur(s).");
Console.WriteLine($" Surtout : seul Z3 PROUVE que {chromatic} est minimal (2 couleurs = UNSAT).");Coloration optimale Z3 (chi = 3) :
Couleurs utilisees : 3
Sommet 0 -> couleur 0
Sommet 1 -> couleur 1
Sommet 2 -> couleur 2
Sommet 3 -> couleur 0
Sommet 4 -> couleur 1
Sommet 5 -> couleur 1
Sommet 6 -> couleur 0
Sommet 7 -> couleur 0
Sommet 8 -> couleur 2
Sommet 9 -> couleur 2
Coloration valide (aucune arete monochrome) : True
=== Comparaison ===
Glouton first-fit (ordre naturel) : 3 couleurs
Glouton first-fit (ordre defavorable): 4 couleurs
Z3 (optimum PROUVE) : 3 couleurs
Dans le pire ordre, le glouton gaspille 1 couleur(s).
Surtout : seul Z3 PROUVE que 3 est minimal (2 couleurs = UNSAT).| Critère | Glouton first-fit | Z3.Linq (recherche de χ) |
|---|---|---|
| Garantie d’optimalité | Aucune (dépend de l’ordre) | Oui (χ prouvé minimal) |
| Preuve d’infaisabilité | Impossible | Oui (UNSAT pour k < χ) |
| Coût | Linéaire, instantané | NP-difficile, mais trivial à cette échelle |
| Couleurs sur Petersen | 3 (ordre favorable) ou 4 (ordre défavorable) | 3 (optimum prouvé) |
Le graphe de Petersen illustre pourquoi la coloration est un vrai problème combinatoire : pas de clique de taille 4 (rien ne « force » visuellement une quatrième couleur), et pourtant le first-fit peut y dépenser une couleur de trop selon l’ordre — sans jamais pouvoir le détecter. Le solveur, lui, raisonne globalement, certifie le minimum, et prouve qu’aucune 2-coloration n’existe — exactement la valeur ajoutée de l’approche déclarative sur une structure irrégulière.
À retenir : un problème dégénéré (graphe biparti, ordre favorable) ne distinguerait pas le glouton du solveur. Le choix de Petersen, structure non triviale au nombre chromatique non évident, est ce qui met la capacité du moteur en valeur.
Ajoutez au graphe de Petersen une arête supplémentaire qui crée une clique de taille 4 (quatre sommets tous deux à deux adjacents), puis relancez la recherche du nombre chromatique. Vérifiez que χ passe à 4.
Indices : - Une clique de taille 4 nécessite au moins 4 couleurs (chaque sommet de la clique doit différer de tous les autres). - Repérez quatre sommets et ajoutez les arêtes manquantes entre eux dans une copie de la liste edges. - Réutilisez la structure de la boucle de recherche en ajoutant les .Where(...) correspondants.
// Exercice 1 : ajouter une arete creant une clique de taille 4, recalculer chi
// Etape 1 : choisir 4 sommets et lister les aretes a ajouter pour qu'ils forment une clique
// Etape 2 : construire un nouveau theoreme avec les aretes supplementaires
// Etape 3 : relancer la recherche lineaire et verifier chi == 4
// Votre code ici
Console.WriteLine("Exercice 1 a completer");Exercice 1 a completerReformulez le problème en planification d’examens : chaque sommet est un examen, chaque arête signifie qu’un étudiant suit les deux examens (ils ne peuvent donc pas être au même créneau), et chaque couleur est un créneau horaire. Construisez votre propre graphe de conflits (au moins 6 examens) et trouvez le nombre minimal de créneaux.
Indices : - La modélisation est identique à la coloration : seul le vocabulaire change (couleur → créneau). - Choisissez les conflits de sorte que le glouton et le solveur diffèrent, pour illustrer le gain. - Affichez l’emploi du temps : pour chaque créneau, la liste des examens qui s’y déroulent.
// Exercice 2 : planification d'examens (coloration deguisee)
// Etape 1 : definir votre graphe de conflits (sommets = examens, aretes = etudiants communs)
// Etape 2 : trouver le nombre minimal de creneaux via la recherche lineaire
// Etape 3 : afficher l'emploi du temps par creneau
// Votre code ici
Console.WriteLine("Exercice 2 a completer");Exercice 2 a completerPour k = 3 couleurs (sans la brisure de symétrie C0 = 0), combien de colorations valides distinctes le graphe de Petersen admet-il ? Approchez la réponse en énumérant les solutions : après chaque solution trouvée, ajoutez une contrainte qui exclut cette assignation précise, puis relancez, jusqu’à UNSAT.
Indices : - Le nombre de 3-colorations du graphe de Petersen est 120 (avec les permutations de couleurs). - Pour exclure une solution s, ajoutez une contrainte ¬(C0 == s0 && C1 == s1 && … ), c.-à-d. au moins une variable diffère. - Attention : sans brisure de symétrie, chaque coloration « géométrique » est comptée 3! = 6 fois (permutations des noms de couleurs).
// Exercice 3 : compter les 3-colorations en enumerant les solutions
// Etape 1 : boucle qui resout, puis exclut la solution trouvee, jusqu'a UNSAT
// Etape 2 : compter les solutions ; comparer a 120
// Etape 3 : diviser par 3! = 6 pour obtenir les colorations a permutation pres
// Votre code ici
Console.WriteLine("Exercice 3 a completer");Exercice 3 a completer? : -> MkIte)Ce notebook colore le graphe sous une contrainte dure : deux sommets adjacents ont des couleurs différentes. Mais une technique de modelisation fondamentale consiste a reifier une condition en un indicateur 0/1 - condition ? 1 : 0 - pour la compter au lieu de l’interdire. On passe alors d’un « aucune arete n’est monochrome » (dur) a un « au plus k aretes monochromes » (souple), en sommant les indicateurs de conflit. C’est le bloc de base des penalites MaxSAT et de tout comptage de contraintes.
Cote DSL, une telle reification n’etait pas exprimable avant le binding B2 : un ternaire C# dans un .Where(...) levait NotSupportedException (le visiteur n’avait pas de cas Conditional). Le binding ajoute VisitConditional qui traduit cond ? a : b en MkITE(test, ifTrue, ifFalse) - le ternaire devient un indicateur Z3 de première classe.
Stack : A + B - pourquoi. On modelise un triangle (3 sommets tous adjacents) avec 2 couleurs seulement : un 2-coloriage propre est impossible (un triangle exige 3 couleurs). Plutot que de constater l’insatisfiabilite, on compte les conflits : pour chaque arete
(u,v), l’indicateur de conflit estcu == cv ? 1 : 0. Cote raw, on reifie a la main chaque conflit enMkITE(MkEq(cu,cv), MkInt(1), MkInt(0))puis on somme viaMkAdd. Cote DSL, la même reification s’ecrit en ternaire C# naturel(cu == cv ? 1 : 0)dans le lambda. Le contraste :somme <= 1est SAT (un triangle bicolore a toujours au moins 1 conflit),somme == 0est UNSAT (preuve que le nombre chromatique depasse 2) - obtenu des deux cotes sur le même modèle.
// B2 - Indicateurs conditionnels "MkIte" : deux stacks sur le MEME triangle sous-colore.
// Triangle : sommets A, B, C tous adjacents (aretes A-B, B-C, A-C). Palette : 2 couleurs {0, 1}.
// Un 2-coloriage PROPRE est impossible (triangle => chi = 3). On COMPTE les conflits au lieu de les interdire :
// conflit d'arete = (cu == cv ? 1 : 0). Contrainte souple : somme des conflits <= 1 (SAT) ; == 0 (UNSAT, prouve chi > 2).
// Classe au niveau cellule (requise par NewTheorem<T>) : trois couleurs de sommet.
public class TriColor2 { public int A { get; set; } public int B { get; set; } public int C { get; set; } }
// =====================================================================
// BLOC RAW (API brute Microsoft.Z3) : chaque conflit reifie a la main en MkITE(cond, 1, 0)
// =====================================================================
{
using var z3 = new Microsoft.Z3.Context();
IntExpr a = z3.MkIntConst("a"), b = z3.MkIntConst("b"), c = z3.MkIntConst("c");
var palette = new Microsoft.Z3.BoolExpr[] {
z3.MkGe(a, z3.MkInt(0)), z3.MkLe(a, z3.MkInt(1)),
z3.MkGe(b, z3.MkInt(0)), z3.MkLe(b, z3.MkInt(1)),
z3.MkGe(c, z3.MkInt(0)), z3.MkLe(c, z3.MkInt(1)),
};
// Indicateurs de conflit : (cu == cv ? 1 : 0) reifies en MkITE
ArithExpr iAB = (ArithExpr)z3.MkITE(z3.MkEq(a, b), z3.MkInt(1), z3.MkInt(0));
ArithExpr iBC = (ArithExpr)z3.MkITE(z3.MkEq(b, c), z3.MkInt(1), z3.MkInt(0));
ArithExpr iAC = (ArithExpr)z3.MkITE(z3.MkEq(a, c), z3.MkInt(1), z3.MkInt(0));
ArithExpr conflicts = z3.MkAdd(iAB, iBC, iAC);
// Souple : au plus 1 conflit
var sSoft = z3.MkSolver();
sSoft.Assert(palette);
sSoft.Assert(z3.MkLe(conflicts, z3.MkInt(1)));
Status stSoft = sSoft.Check();
Console.WriteLine($"[RAW] conflits <= 1 : {stSoft}");
if (stSoft == Status.SATISFIABLE) {
var m = sSoft.Model;
var cnt = (IntNum)m.Eval(conflicts, true);
Console.WriteLine($"[RAW] coloriage : A={m.Eval(a,true)}, B={m.Eval(b,true)}, C={m.Eval(c,true)} (conflits={cnt})");
}
// Dur : zero conflit (2-coloriage propre) -> UNSAT
var sHard = z3.MkSolver();
sHard.Assert(palette);
sHard.Assert(z3.MkEq(conflicts, z3.MkInt(0)));
Console.WriteLine($"[RAW] conflits == 0 : {sHard.Check()} (2 couleurs ne suffisent pas pour un triangle)");
}
// =====================================================================
// BLOC DSL (Z3.Linq) : la meme reification en ternaire C# naturel (cond ? 1 : 0)
// =====================================================================
{
using var thCtx = new Z3Context();
// Souple : au plus 1 conflit
var soft = thCtx.NewTheorem<TriColor2>()
.Where(t => t.A >= 0).Where(t => t.A <= 1)
.Where(t => t.B >= 0).Where(t => t.B <= 1)
.Where(t => t.C >= 0).Where(t => t.C <= 1)
.Where(t => (t.A == t.B ? 1 : 0) + (t.B == t.C ? 1 : 0) + (t.A == t.C ? 1 : 0) <= 1)
.Solve();
if (soft != null) {
int cnt = (soft.A == soft.B ? 1 : 0) + (soft.B == soft.C ? 1 : 0) + (soft.A == soft.C ? 1 : 0);
Console.WriteLine($"[DSL] conflits <= 1 : SAT -> A={soft.A}, B={soft.B}, C={soft.C} (conflits={cnt})");
}
// Dur : zero conflit -> UNSAT (le ternaire indicateur prouve chi > 2)
var hard = thCtx.NewTheorem<TriColor2>()
.Where(t => t.A >= 0).Where(t => t.A <= 1)
.Where(t => t.B >= 0).Where(t => t.B <= 1)
.Where(t => t.C >= 0).Where(t => t.C <= 1)
.Where(t => (t.A == t.B ? 1 : 0) + (t.B == t.C ? 1 : 0) + (t.A == t.C ? 1 : 0) == 0)
.Solve();
Console.WriteLine($"[DSL] conflits == 0 : {(hard == null ? "UNSAT" : "SAT?!")} -> 2 couleurs insuffisantes, chi(triangle) = 3");
}[RAW] conflits <= 1 : SATISFIABLE
[RAW] coloriage : A=1, B=0, C=0 (conflits=1)
[RAW] conflits == 0 : UNSATISFIABLE (2 couleurs ne suffisent pas pour un triangle)
[DSL] conflits <= 1 : SAT -> A=1, B=0, C=0 (conflits=1)
[DSL] conflits == 0 : UNSAT -> 2 couleurs insuffisantes, chi(triangle) = 3Les deux stacks modelisent le même triangle sous-colore et comptent les mêmes conflits via des indicateurs cu == cv ? 1 : 0. Les deux verdicts coincident : somme <= 1 SAT (un triangle bicolore a au moins un conflit) et somme == 0 UNSAT (donc chi > 2). La différence est comment on ecrit l’indicateur :
| Aspect | RAW (MkITE) |
DSL (ternaire ? :) |
|---|---|---|
| Reification | MkITE(MkEq(cu,cv), MkInt(1), MkInt(0)) |
(cu == cv ? 1 : 0) (C# idiomatique) |
| Cast necessaire | Oui : (ArithExpr) pour sommer |
Non : le type est inference |
| Somme | MkAdd(iAB, iBC, iAC) |
+ C# natif |
| Avant B2 | (toujours disponible en raw) | NotSupportedException sur le Conditional |
Ligne de contraste (a retenir) : le raw construit l’indicateur comme un terme Z3 explicite (
MkITE+ cast +MkAdd) ; le DSL laisse ecrire l’indicateur comme un ternaire C# ordinaire -(cu == cv ? 1 : 0)- queVisitConditionaltraduit enMkITE. Même comptage de conflits, deux notations : termes Z3 d’un cote, expression C# de l’autre. L’indicateur reifie est ce qui fait passer d’un modèle dur (interdire) a un modèle souple (compter et borner).
Cas d’usage : la reification cond ? 1 : 0 est le bloc de base des contraintes de cardinalite (« au plus / au moins k parmi ces conditions ») et des penalites souples (MaxSAT via Optimize). Dans la coloration, elle transforme le coloriage propre (dur, parfois UNSAT) en minimisation de conflits (toujours SAT). On garde le raw pour un MkITE dont les branches sont des termes Z3 arbitraires (tableaux, fonctions non-interpretees) hors du schema du modèle-objet.
Ce notebook a transposé le paradigme déclaratif de Z3.Linq à une structure de graphe irrégulière — un terrain différent des grilles (Sudoku) et des ordonnancements linéaires (job shop). Trois enseignements :
χ = 3 et démontre l’infaisabilité à 2 couleurs. La preuve d’optimalité (UNSAT en dessous de χ) est hors de portée d’une heuristique.Pour aller plus loin : la coloration sous-tend l’allocation de registres (compilation), l’attribution de fréquences, et la planification ; les mêmes contraintes, à plus grande échelle, motivent les solveurs SAT/SMT industriels.
Navigation : << 11 Job Shop Scheduling | Index Z3 | Index SymbolicAI