Twin C# de Z3-02-Sudoku-Python.ipynb (parité .NET, marathon #4956, suite de Z3-Python-01-Introduction-Csharp).
Navigation : Index | Index SMT | Index SymbolicAI | << 01 - Introduction (C#) | 03 - Tactics (C#) >>
Ce notebook résout le Sudoku de façon déclarative avec le moteur réel Microsoft.Z3 (NuGet, Z3 4.12.2.0) — le même solveur que z3-solver (Python). Au lieu d’écrire un algorithme de backtracking, on exprime les règles du Sudoku comme des contraintes et le solveur trouve la solution. C’est le paradigme SMT (Satisfiability Modulo Theories) : on spécifie le quoi (les contraintes), jamais le comment (la recherche).
Une grille de Sudoku 9×9 respecte trois contraintes d’unicité :
La contrainte Z3 clé est MkDistinct : elle impose que tous les termes d’un ensemble soient deux à deux distincts — elle encode exactement la règle « tous différents » du Sudoku.
Résoudre un Sudoku à la main = backtracking (essayer un chiffre, propager, revenir en arrière si contradiction). Z3 fait de même, mais avec un algorithme SOTA : CDCL (Conflict-Driven Clause Learning) + propagation d’intervalles, qui apprend de chaque conflit pour accélérer la recherche. Sur une instance 9×9, la résolution est quasi instantanée — et la vraie force du déclaratif est la généralité : le même Solver résout aussi l’Exercice 1 (anti-diagonale) en ajoutant une seule contrainte, sans réécrire d’algorithme.
Solver + MkDistinct.#r "nuget: Microsoft.Z3"
#load "Z3NativeLoader.cs"
using Microsoft.Z3;
using System.Text;
// Bibliotheque native de Z3 hors Windows et macOS Intel (voir Z3NativeLoader.cs)
Z3NativeLoader.Register(typeof(Context).Assembly);
Console.WriteLine("Imports OK : Microsoft.Z3 version " + Microsoft.Z3.Version.FullVersion);Imports OK : Microsoft.Z3 version Z3 4.12.2.0Microsoft.Z3 version Z3 4.12.2.0 — c’est le même solveur que z3-solver côté Python (Z3Prover/z3, développé par Microsoft Research). Le binding .NET via NuGet expose l’API managée (Context, Solver, IntExpr, MkDistinct, MkEq). Aucun algorithme de résolution n’est écrit dans ce notebook : on déclare le problème, Z3 le résout — le paradigme déclaratif (SMT) opposé au backtracking impératif. Le moteur fait tout le travail de recherche ; nous, nous modélisons.
Deux puzzles de test. 0 = case vide. Le puzzle facile (grille canonique Wikipedia) donne 30 indices, l’intermediaire en donne 36.
// Puzzle facile : 30 indices donnes.
int[][] puzzle_facile = new int[][] {
new int[] {5, 3, 0, 0, 7, 0, 0, 0, 0},
new int[] {6, 0, 0, 1, 9, 5, 0, 0, 0},
new int[] {0, 9, 8, 0, 0, 0, 0, 6, 0},
new int[] {8, 0, 0, 0, 6, 0, 0, 0, 3},
new int[] {4, 0, 0, 8, 0, 3, 0, 0, 1},
new int[] {7, 0, 0, 0, 2, 0, 0, 0, 6},
new int[] {0, 6, 0, 0, 0, 0, 2, 8, 0},
new int[] {0, 0, 0, 4, 1, 9, 0, 0, 5},
new int[] {0, 0, 0, 0, 8, 0, 0, 7, 9},
};
// Puzzle intermediaire : 36 indices donnes.
int[][] puzzle_intermediaire = new int[][] {
new int[] {0, 0, 0, 2, 6, 0, 7, 0, 1},
new int[] {6, 8, 0, 0, 7, 0, 0, 9, 0},
new int[] {1, 9, 0, 0, 0, 4, 5, 0, 0},
new int[] {8, 2, 0, 1, 0, 0, 0, 4, 0},
new int[] {0, 0, 4, 6, 0, 2, 9, 0, 0},
new int[] {0, 5, 0, 0, 0, 3, 0, 2, 8},
new int[] {0, 0, 9, 3, 0, 0, 0, 7, 4},
new int[] {0, 4, 0, 0, 5, 0, 0, 3, 6},
new int[] {7, 0, 3, 0, 1, 8, 0, 0, 0},
};
int CompterIndices(int[][] g) {
int n = 0;
for (int r = 0; r < 9; r++) for (int c = 0; c < 9; c++) if (g[r][c] != 0) n++;
return n;
}
Console.WriteLine("Puzzle facile : " + CompterIndices(puzzle_facile) + " indices donnes");
Console.WriteLine("Puzzle intermediaire : " + CompterIndices(puzzle_intermediaire) + " indices donnes");Puzzle facile : 30 indices donnes
Puzzle intermediaire : 36 indices donnesLe puzzle facile (30 indices, grille canonique Wikipedia) laisse 51 cases vides ; l’intermédiaire (36 indices) n’en laisse que 45. Contre-intuitivement, plus d’indices ≠ plus facile : la difficulté d’un Sudoku dépend de la profondeur de déduction requise (chaînes de conséquences, techniques avancées comme X-Wing ou Swordfish), pas seulement du nombre de cases vides. Pour Z3, ces deux puzzles sont triviaux : un solveur SMT résout n’importe quel Sudoku légitime en millisecondes, quelle que soit sa difficulté humaine perçue — la complexité théorique (NP-complétude) n’opère qu’à l’échelle de la classe de problèmes, pas sur une instance 9×9 moderne.
La fonction ResoudreSudoku construit un Solver Z3 et pose les contraintes :
MkEq).MkDistinct.Puis s.Check() : si SATISFIABLE, on extrait le modèle. Aucun backtracking n’est ecrit a la main : c’est le moteur Z3 qui cherche.
int[][] ResoudreSudoku(Context ctx, int[][] grille)
{
var s = ctx.MkSolver();
// Variables : 81 entiers c_r_c
var cellules = new IntExpr[9][];
for (int r = 0; r < 9; r++) {
cellules[r] = new IntExpr[9];
for (int c = 0; c < 9; c++) cellules[r][c] = ctx.MkIntConst("c_" + r + "_" + c);
}
// 1. Domaine : 1 <= cellule <= 9
for (int r = 0; r < 9; r++) for (int c = 0; c < 9; c++) {
s.Add(ctx.MkGe(cellules[r][c], ctx.MkInt(1)));
s.Add(ctx.MkLe(cellules[r][c], ctx.MkInt(9)));
}
// 2. Indices : figer les cases pre-remplies
for (int r = 0; r < 9; r++) for (int c = 0; c < 9; c++)
if (grille[r][c] != 0) s.Add(ctx.MkEq(cellules[r][c], ctx.MkInt(grille[r][c])));
// 3a. Unicite par ligne
for (int r = 0; r < 9; r++) {
var ligne = new IntExpr[9];
for (int c = 0; c < 9; c++) ligne[c] = cellules[r][c];
s.Add(ctx.MkDistinct(ligne));
}
// 3b. Unicite par colonne
for (int c = 0; c < 9; c++) {
var col = new IntExpr[9];
for (int r = 0; r < 9; r++) col[r] = cellules[r][c];
s.Add(ctx.MkDistinct(col));
}
// 3c. Unicite par bloc 3x3
for (int br = 0; br < 3; br++) for (int bc = 0; bc < 3; bc++) {
var bloc = new IntExpr[9]; int k = 0;
for (int i = 0; i < 3; i++) for (int j = 0; j < 3; j++) bloc[k++] = cellules[3*br + i][3*bc + j];
s.Add(ctx.MkDistinct(bloc));
}
if (s.Check() == Status.SATISFIABLE)
{
var m = s.Model;
int[][] sol = new int[9][];
for (int r = 0; r < 9; r++) {
sol[r] = new int[9];
for (int c = 0; c < 9; c++) sol[r][c] = (int)((IntNum)m.Evaluate(cellules[r][c])).Int64;
}
return sol;
}
return null;
}
var ctxS = new Context();
var solution_facile = ResoudreSudoku(ctxS, puzzle_facile);
Console.WriteLine("Puzzle facile : " + (solution_facile != null ? "resolu" : "insatisfiable"));Puzzle facile : resoluPuzzle facile : resolu. La fonction n’a écrit aucune recherche : 81 variables entières, 27 contraintes MkDistinct (9 lignes + 9 colonnes + 9 blocs 3×3), les pré-remplissages figés par MkEq — puis s.Check() retourne SATISFIABLE. Le moteur Z3 a fait tout le travail via CDCL + propagation d’intervalles, l’algorithme SOTA de la résolution SAT/SMT. C’est tout l’intérêt de l’approche déclarative : on spécifie le problème (ses contraintes), jamais sa méthode de résolution. MkDistinct est l’abstraction centrale : « tous différents » encode exactement la règle du Sudoku, et se généralise à tout CSP d’unicité (N-Reines, graph coloring, emploi du temps).
Le twin Python utilise matplotlib pour afficher la grille. Ce twin C# propose une visualisation ASCII equivalente : les cases données sont en gras ([n]), les cases calculees par Z3 en clair (n). Les separateurs | et --+---+-- marquent les blocs 3x3.
void AfficherSudoku(int[][] grille, int[][] donnees = null, string titre = "Sudoku")
{
Console.WriteLine("--- " + titre + " ---");
for (int r = 0; r < 9; r++) {
var sb = new StringBuilder();
for (int c = 0; c < 9; c++) {
int v = grille[r][c];
bool donne = (donnees != null && donnees[r][c] != 0);
if (v == 0) sb.Append(" . ");
else if (donne) sb.Append("[" + v + "]");
else sb.Append(" " + v + " ");
if (c == 2 || c == 5) sb.Append("|");
}
Console.WriteLine(sb);
if (r == 2 || r == 5) Console.WriteLine("-----------+-----------+-----------");
}
}
AfficherSudoku(puzzle_facile, puzzle_facile, "Puzzle facile (enonce, indices entre crochets)");
Console.WriteLine();
if (solution_facile != null) AfficherSudoku(solution_facile, puzzle_facile, "Solution (Z3)");--- Puzzle facile (enonce, indices entre crochets) ---
[5][3] . | . [7] . | . . .
[6] . . |[1][9][5]| . . .
. [9][8]| . . . | . [6] .
-----------+-----------+-----------
[8] . . | . [6] . | . . [3]
[4] . . |[8] . [3]| . . [1]
[7] . . | . [2] . | . . [6]
-----------+-----------+-----------
. [6] . | . . . |[2][8] .
. . . |[4][1][9]| . . [5]
. . . | . [8] . | . [7][9]
--- Solution (Z3) ---
[5][3] 4 | 6 [7] 8 | 9 1 2
[6] 7 2 |[1][9][5]| 3 4 8
1 [9][8]| 3 4 2 | 5 [6] 7
-----------+-----------+-----------
[8] 5 9 | 7 [6] 1 | 4 2 [3]
[4] 2 6 |[8] 5 [3]| 7 9 [1]
[7] 1 3 | 9 [2] 4 | 8 5 [6]
-----------+-----------+-----------
9 [6] 1 | 5 3 7 |[2][8] 4
2 8 7 |[4][1][9]| 6 3 [5]
3 4 5 | 2 [8] 6 | 1 [7][9]La visualisation distingue les indices donnés [n] (cases de l’énoncé, figées par MkEq) des cases calculées n (remplies par Z3). On vérifie d’un coup d’œil les trois règles : chaque ligne, colonne et bloc 3×3 contient 1-9 sans répétition. La solution est unique pour un puzzle bien posé — l’Exercice 3 le confirmera en énumérant les solutions (UNSAT après blocage de la première = unicité). Le twin Python affiche cette même grille en couleur via matplotlib ; la version ASCII du twin C# est iso-informative (Prong B EPIC #3801) : mêmes données structurales (donné vs calculé, séparation des blocs), modalité de rendu différente, sans dépendance graphique.
Trois exercices a completer. Les stubs retournent null : a vous d’implementer la resolution avec Z3.
// EXERCICE 1 : Resoudre le Sudoku avec une contrainte d anti-diagonale.
// L anti-diagonale (cellules (0,8),(1,7),...,(8,0)) doit elle aussi etre composee de chiffres distincts.
// Indice : ajoutez un MkDistinct sur ces 9 cellules AVANT de resoudre.
// Etape 1 : recuperer les 9 cellules de l anti-diagonale cellules[i][8-i]
// Etape 2 : s.Add(ctx.MkDistinct(anti_diag))
// Etape 3 : Check() et retourner la solution
int[][] ResoudreAvecAntiDiagonale(Context ctx, int[][] grille)
{
// TODO etudiant : implementez la resolution avec contrainte d anti-diagonale
return null; // TODO etudiant : remplacer par la solution trouvee
}
var sol_ex1 = ResoudreAvecAntiDiagonale(new Context(), puzzle_facile);
Console.WriteLine("Exercice 1 (anti-diagonale) : " + (sol_ex1 != null ? "resolu" : "(a completer)"));Exercice 1 (anti-diagonale) : (a completer)// EXERCICE 2 : Resoudre et visualiser le puzzle intermediaire.
// Indice : appelez ResoudreSudoku sur puzzle_intermediaire puis AfficherSudoku.
// Etape 1 : var sol = ResoudreSudoku(new Context(), puzzle_intermediaire);
// Etape 2 : AfficherSudoku(sol, puzzle_intermediaire, "Solution intermediaire");
void ResoudreEtAfficherIntermediaire()
{
// TODO etudiant : resoudre le puzzle intermediaire et l afficher
Console.WriteLine("(a completer)");
}
ResoudreEtAfficherIntermediaire();(a completer)// EXERCICE 3 : Compter le nombre de solutions (jusqu a 2).
// Indice : apres une solution, ajoutez une contrainte qui bloque celle-ci puis re-checkez.
// Etape 1 : resoudre une premiere fois
// Etape 2 : si SAT, ajouter s.Add(MkOr( cellule != valeur_pour_chaque_cellule )) pour bloquer la solution
// Etape 3 : re-checker ; SAT = au moins 2 solutions, UNSAT = solution unique
int CompterSolutions(Context ctx, int[][] grille, int limite = 2)
{
// TODO etudiant : comptez le nombre de solutions jusqu a limite
return 0; // TODO etudiant : remplacer par le nombre de solutions trouvees
}
int nb = CompterSolutions(new Context(), puzzle_facile, 2);
Console.WriteLine("Exercice 3 (nombre de solutions) : " + (nb > 0 ? nb.ToString() : "(a completer)"));Exercice 3 (nombre de solutions) : (a completer)Ce twin C# couvre les mêmes concepts que la version Python : modelisation declarative d’un CSP (le Sudoku), contrainte d’unicite MkDistinct sur les lignes / colonnes / blocs, extraction du modèle, et exercices d’extension (anti-diagonale, enumeration des solutions).
La visualisation ASCII remplace matplotlib (twin Python) : c’est une valeur complementaire (Prong B EPIC #3801) – la même information structurelle (indices donnes vs calcules, separation des blocs) rendue dans une modalite différente, sans dépendance graphique.
Le binding Microsoft.Z3 resout le Sudoku exactement comme z3-solver (Python) : aucun backtracking n’est ecrit, le moteur SOTA fait tout.