← 12 — Graph Coloring Petersen | README Z3
Navigation : Index Z3 | Index SymbolicAI | Index général
Theorem<T> de Z3.Linq avec variables entières simples (pas de tableaux) et la contrainte globale DistinctDurée estimée : 35-45 minutes
Un cryptarithme (ou alphamétique) est une équation où chaque lettre représente un chiffre distinct. Le classique absolu :
S E N D
+ M O R E
---------
M O N E YChaque lettre (S, E, N, D, M, O, R, Y) est un chiffre de 0 à 9, toutes différentes, et les lettres de tête (S pour SEND, M pour MORE et MONEY) ne peuvent pas valoir 0 (sinon le nombre aurait un zéro non-significatif). L’égalité arithmétique doit être vérifiée.
C’est l’archétype d’un problème où la modélisation déclarative bat l’énumération brutale : il y a 10×9×7×6×5×4×3 ≈ 1,6 million de combinaisons à explorer naïvement pour 8 lettres distinctes, mais la propagation de contraintes du solveur en réduit l’espace drastiquement.
#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.LinqTrois familles de contraintes structurent le problème :
{0, ..., 9} (8 variables entières).Z3Methods.Distinct(...) impose que les 8 lettres prennent des valeurs deux à deux distinctes — c’est le cœur du problème, sans elle l’équation admettrait des solutions triviales.S ≠ 0 et M ≠ 0 (les nombres ne commencent pas par zéro).SEND = 1000·S + 100·E + 10·N + D, MORE = 1000·M + 100·O + 10·R + E, MONEY = 10000·M + 1000·O + 100·N + 10·E + Y. On exige SEND + MORE == MONEY.Le binding Z3.Linq accepte ces expressions arithmétiques linéaires directement dans le lambda .Where(...) : le rewriter les traduit en assertions SMT sur la théorie des entiers (LinearIntegerArithmetic).
// Cryptarithme classique : SEND + MORE = MONEY
public class SendMoreMoney
{
public int S = 0, E = 0, N = 0, D = 0;
public int M = 0, O = 0, R = 0, Y = 0;
}
using (var ctx = new Z3Context())
{
var th = ctx.NewTheorem<SendMoreMoney>();
// (1) Domaine 0..9 pour chaque lettre
th = th.Where(t => t.S >= 0 && t.S <= 9 && t.E >= 0 && t.E <= 9
&& t.N >= 0 && t.N <= 9 && t.D >= 0 && t.D <= 9
&& t.M >= 0 && t.M <= 9 && t.O >= 0 && t.O <= 9
&& t.R >= 0 && t.R <= 9 && t.Y >= 0 && t.Y <= 9);
// (2) Les 8 lettres sont deux à deux distinctes (contrainte globale)
th = th.Where(t => Z3Methods.Distinct(t.S, t.E, t.N, t.D, t.M, t.O, t.R, t.Y));
// (3) Têtes non nulles (pas de zéro non-significatif)
th = th.Where(t => t.S > 0 && t.M > 0);
// (4) Équation arithmétique positionnelle : SEND + MORE == MONEY
th = th.Where(t =>
(1000 * t.S + 100 * t.E + 10 * t.N + t.D) +
(1000 * t.M + 100 * t.O + 10 * t.R + t.E) ==
(10000 * t.M + 1000 * t.O + 100 * t.N + 10 * t.E + t.Y));
var sol = th.Solve();
if (sol == null) {
Console.WriteLine("UNSAT : aucune solution (inattendu pour ce cryptarithme)");
} else {
int send = 1000 * sol.S + 100 * sol.E + 10 * sol.N + sol.D;
int more = 1000 * sol.M + 100 * sol.O + 10 * sol.R + sol.E;
int money = 10000 * sol.M + 1000 * sol.O + 100 * sol.N + 10 * sol.E + sol.Y;
Console.WriteLine($" S={sol.S} E={sol.E} N={sol.N} D={sol.D} M={sol.M} O={sol.O} R={sol.R} Y={sol.Y}");
Console.WriteLine($" {send,5}");
Console.WriteLine($" + {more,5}");
Console.WriteLine($" -------");
Console.WriteLine($" {money,5} ({send} + {more} = {money}, vérifié = {send + more == money})");
}
} S=9 E=5 N=6 D=7 M=1 O=0 R=8 Y=2
9567
+ 1085
-------
10652 (9567 + 1085 = 10652, vérifié = True)Z3 trouve la solution unique en quelques millisecondes :
SEND = 9567, MORE = 1085, MONEY = 106529567 + 1085 = 10652 ✓S=9, E=5, N=6, D=7, M=1, O=0, R=8, Y=2Pourquoi le solveur fait la différence (Prong-B) : la résolution humaine procède colonne par colonne en propagant les retenues (D+E=Y ou Y+10, etc.), ce qui demande une analyse de cas à chaque étape. Le solveur, lui, propage globalement toutes les contraintes simultanément : dès que M=1 est forcé (car SEND + MORE < 20000 implique MONEY < 20000 donc M=1), le reste se déduit par réduction de domaine. Là où un humain explore ~15 minutes, Z3 explore l’arbre de recherche réduit à quelques nœuds.
C’est aussi un exemple où la contrainte globale Distinct est essentielle : sans elle, l’équation arithmétique seule admettrait des solutions où deux lettres prendraient la même valeur (triviales et non-pédagogiques).
Pour mesurer l’écart (et ne pas se contenter d’une affirmation littéraire), comparons deux stratégies sur le même cryptarithme SEND + MORE = MONEY :
{0..9}, soit P(10,8) = 10·9·8·7·6·5·4·3 = 1 814 400 candidats, et tester l’équation pour chacun.Distinct + équation) et laisser le solveur propager.La différence n’est pas tant dans le code (les deux tiennent en quelques lignes) que dans la manière d’explorer : la brute force teste aveuglément 1,8 million de candidats, tandis que Z3 propage — par exemple SEND + MORE < 20000 force immédiatement M = 1, ce qui élimine d’emblée l’essentiel du domaine sans aucun essai.
using System.Diagnostics;
// (1) Brute force : 8 boucles imbriquées, on saute dès que deux lettres coincident
// P(10,8) = 1 814 400 candidats distincts testes.
int nbBrute = 0;
var swBrute = Stopwatch.StartNew();
for (int S=0; S<=9; S++)
for (int E=0; E<=9; E++) { if (E==S) continue;
for (int N=0; N<=9; N++) { if (N==S||N==E) continue;
for (int D=0; D<=9; D++) { if (D==S||D==E||D==N) continue;
for (int M=0; M<=9; M++) { if (M==S||M==E||M==N||M==D) continue;
for (int O=0; O<=9; O++) { if (O==S||O==E||O==N||O==D||O==M) continue;
for (int R=0; R<=9; R++) { if (R==S||R==E||R==N||R==D||R==M||R==O) continue;
for (int Y=0; Y<=9; Y++) { if (Y==S||Y==E||Y==N||Y==D||Y==M||Y==O||Y==R) continue;
if (S>0 && M>0) {
int send = 1000*S + 100*E + 10*N + D;
int more = 1000*M + 100*O + 10*R + E;
int money = 10000*M + 1000*O + 100*N + 10*E + Y;
if (send + more == money) { nbBrute++; }
}
}}}}}}}
swBrute.Stop();
// (2) Z3 : même théorème que la cellule 3, mesuré
var swZ3 = Stopwatch.StartNew();
int nbZ3 = 0;
using (var ctx = new Z3Context())
{
var th = ctx.NewTheorem<SendMoreMoney>()
.Where(t => t.S>=0&&t.S<=9&&t.E>=0&&t.E<=9&&t.N>=0&&t.N<=9&&t.D>=0&&t.D<=9
&&t.M>=0&&t.M<=9&&t.O>=0&&t.O<=9&&t.R>=0&&t.R<=9&&t.Y>=0&&t.Y<=9)
.Where(t => Z3Methods.Distinct(t.S,t.E,t.N,t.D,t.M,t.O,t.R,t.Y))
.Where(t => t.S>0 && t.M>0)
.Where(t => (1000*t.S+100*t.E+10*t.N+t.D)+(1000*t.M+100*t.O+10*t.R+t.E)
==(10000*t.M+1000*t.O+100*t.N+10*t.E+t.Y));
var sol = th.Solve();
if (sol != null) nbZ3 = 1;
}
swZ3.Stop();
Console.WriteLine($"Brute force : {nbBrute} solution(s) en {swBrute.Elapsed.TotalMilliseconds:F1} ms (1 814 400 candidats testes)");
Console.WriteLine($"Z3 solve : {nbZ3} solution(s) en {swZ3.Elapsed.TotalMilliseconds:F1} ms (propagation de contraintes)");
Console.WriteLine($" -> meme resultat ({nbBrute==nbZ3}), strategies differentes.");Brute force : 1 solution(s) en 87,8 ms (1 814 400 candidats testes)
Z3 solve : 1 solution(s) en 47,1 ms (propagation de contraintes)
-> meme resultat (True), strategies differentes.Sur ce petit cryptarithme (8 lettres), les deux approches trouvent la même solution unique en quelques dizaines de millisecondes — l’écart de vitesse brut reste modeste (même ordre de grandeur). C’est attendu : 1,8 million de candidats est un volume digérable pour une boucle C# native, et l’amorçage à froid du solveur pèse sur un petit cas. Le vrai gain du solveur n’est donc pas la vitesse brute sur un exemple jouet, mais trois propriétés qui apparaissent sur des instances plus lourdes : Le vrai gain du solveur n’est donc pas la vitesse brute sur un cas jouet, mais trois propriétés qui apparaissent sur des instances plus lourdes :
Distinct + équation) s’adapte à n’importe quel cryptarithme sans réécrire la logique de recherche — la cellule variante CROSS + ROADS = DANGER le montre (9 lettres, zéro ligne de code de parcours ajoutée).M = 1 sans aucun essai (puisque SEND + MORE < 20000), puis réduit les domaines en cascade. La brute force, elle, teste aussi tous les cas M = 0, 2, ..., 9 avant d’arriver à M = 1.P(10,k) explose (P(10,10) = 3,6 millions, et la combinatoire d’un cryptarithme multiplicatif ou d’une équation à 5 nombres devient vite hors de portée d’une énumération exhaustive), alors que la propagation conserve un coût quasi polynomial.C’est l’illustration concrète du Prong-B : un problème où le moteur SMT n’est pas réduit à un if, mais exerce sa capacité distinctive — réduire un espace combinatoire par propagation de contraintes plutôt que l’énumérer.
Cryptarithme plus long (10 lettres distinctes), qui illustre que le même schéma de modélisation s’adapte sans changement de structure — seules les variables et l’équation diffèrent.
// Variante : CROSS + ROADS = DANGER (10 lettres distinctes)
public class CrossRoads
{
public int C = 0, R = 0, O = 0, S = 0;
public int A = 0, D = 0, N = 0, G = 0, E = 0;
// 9 lettres distinctes : C,R,O,S,A,D,N,G,E
}
using (var ctx = new Z3Context())
{
var th = ctx.NewTheorem<CrossRoads>();
// Domaine 0..9 pour les 9 lettres
th = th.Where(t => t.C >= 0 && t.C <= 9 && t.R >= 0 && t.R <= 9 && t.O >= 0 && t.O <= 9
&& t.S >= 0 && t.S <= 9 && t.A >= 0 && t.A <= 9 && t.D >= 0 && t.D <= 9
&& t.N >= 0 && t.N <= 9 && t.G >= 0 && t.G <= 9 && t.E >= 0 && t.E <= 9);
// 9 lettres deux à deux distinctes
th = th.Where(t => Z3Methods.Distinct(t.C, t.R, t.O, t.S, t.A, t.D, t.N, t.G, t.E));
// Têtes non nulles : C (CROSS), R (ROADS), D (DANGER)
th = th.Where(t => t.C > 0 && t.R > 0 && t.D > 0);
// CROSS + ROADS == DANGER
// CROSS = 10000·C + 1000·R + 100·O + 10·S + S
// ROADS = 10000·R + 1000·O + 100·A + 10·D + S
// DANGER = 100000·D + 10000·A + 1000·N + 100·G + 10·E + R
th = th.Where(t =>
(10000 * t.C + 1000 * t.R + 100 * t.O + 10 * t.S + t.S) +
(10000 * t.R + 1000 * t.O + 100 * t.A + 10 * t.D + t.S) ==
(100000 * t.D + 10000 * t.A + 1000 * t.N + 100 * t.G + 10 * t.E + t.R));
var sol = th.Solve();
if (sol == null) {
Console.WriteLine("UNSAT : aucune solution pour CROSS + ROADS = DANGER");
} else {
int cross = 10000 * sol.C + 1000 * sol.R + 100 * sol.O + 10 * sol.S + sol.S;
int roads = 10000 * sol.R + 1000 * sol.O + 100 * sol.A + 10 * sol.D + sol.S;
int danger = 100000 * sol.D + 10000 * sol.A + 1000 * sol.N + 100 * sol.G + 10 * sol.E + sol.R;
Console.WriteLine($"CROSS={cross} ROADS={roads} DANGER={danger} ({cross} + {roads} = {cross + roads}, égal à DANGER = {danger} : {cross + roads == danger})");
}
}CROSS=96233 ROADS=62513 DANGER=158746 (96233 + 62513 = 158746, égal à DANGER = 158746 : True)Les trois exercices ci-dessous vous font réutiliser le patron pour de nouveaux cryptarithmes. Chaque exercice suit le même squelette : définir la classe de variables, ajouter domaine + Distinct + têtes non nulles + équation, puis Solve().
Rappel C.1 : les stubs ne lèvent jamais d’erreur — ils utilisent Console.WriteLine("Exercice à compléter"). Le notebook s’exécute de bout en bout même exercices non résolus.
Résolvez ce cryptarithme classique à 10 lettres (D, O, N, A, L, G, E, R, B, T). Têtes non nulles : D (DONALD), G (GERALD), R (ROBERT).
Étapes : 1. Définissez la classe DonaldGerald avec les 10 propriétés int. 2. Ajoutez le domaine 0..9 pour chacune. 3. Ajoutez Z3Methods.Distinct(...) sur les 10 lettres. 4. Ajoutez les contraintes de tête non nulle (D > 0, G > 0, R > 0). 5. Ajoutez l’équation positionnelle développée.
// Exercice 1 : DONALD + GERALD = ROBERT
// TODO étudiant :
// Étape 1 : classe DonaldGerald { D, O, N, A, L, G, E, R, B, T } (int)
// Étape 2 : domaine 0..9 pour les 10 lettres
// Étape 3 : Z3Methods.Distinct(...) sur les 10 lettres
// Étape 4 : têtes non nulles (D > 0, G > 0, R > 0)
// Étape 5 : équation DONALD + GERALD == ROBERT
// DONALD = 100000·D + 10000·O + 1000·N + 100·A + 10·L + L
// GERALD = 100000·G + 10000·E + 1000·R + 100·A + 10·L + D
// ROBERT = 100000·R + 10000·O + 1000·B + 100·E + 10·R + T
Console.WriteLine("Exercice 1 à compléter : modélisez DONALD + GERALD = ROBERT avec Z3.Linq");Exercice 1 à compléter : modélisez DONALD + GERALD = ROBERT avec Z3.LinqSEND + MORE = MONEY admet une unique solution. Modifiez le théorème de la cellule 3 pour compter toutes les solutions (au lieu de s’arrêter à la première) et confirmer qu’il n’y en a qu’une.
Indice : Z3.Linq ne fournit pas directement un itérateur de toutes les solutions. Une approche consiste à appeler Solve() puis à ajouter une contrainte niant la solution trouvée (!= sur au moins une lettre) et à re-appeler Solve(), jusqu’à obtenir null (UNSAT). Comptez les itérations.
// Exercice 2 : compter toutes les solutions de SEND + MORE = MONEY
// TODO étudiant :
// 1. Boucle : Solve() -> si sol != null, compter++, ajouter contrainte (au moins une lettre != sol)
// 2. Recommencer jusqu'à UNSAT (sol == null)
// 3. Afficher le nombre total de solutions
Console.WriteLine("Exercice 2 à compléter : énumérez toutes les solutions de SEND + MORE = MONEY");Exercice 2 à compléter : énumérez toutes les solutions de SEND + MORE = MONEYModélisez la multiplication : ABC × D = DBC où chaque lettre est un chiffre distinct, A ≠ 0 et D ≠ 0. Attention : ici c’est une multiplication (==), pas une addition — l’équation est ABC * D == DBC (avec ABC = 100·A + 10·B + C).
Question subsidiaire : ce cryptarithme admet-il une solution ? Si oui, combien ?
Exercice 3 à compléter : modélisez ABC × D = DBCLe cryptarithme est le terrain idéal pour appréhender la modélisation déclarative d’un problème combinatoire :
Theorem<T> de Z3.Linq s’applique tel quel.Distinct remplace élégamment l’énumération exhaustive des paires != (28 paires pour 8 lettres, 45 pour 10).Points clés : - Un problème qu’un humain résout en ~15 minutes tombe en millisecondes : la propagation globale écrase l’analyse colonne-par-colonne. - La contrainte Distinct est essentielle — sans elle, l’équation admet des solutions triviales (lettres répétées). - Le même schéma (domaine + Distinct + têtes + équation) s’adapte à tout cryptarithme, quelle que soit sa longueur.
Référence : Dudeney (1924) — “Send More Money”, publié dans le Strand Magazine. Premier cryptarithme largement popularisé.