Sudoku : Théorème Explicite vs Modèle Implicite par Arrays

Navigation : Index SymbolicAI | Serie Z3 | << Introduction Linq2Z3

Objectifs d’apprentissage

A la fin de ce notebook, vous saurez : 1. Modeliser un Sudoku avec 81 proprietes explicites (approche naive) 2. Modeliser un Sudoku avec une seule List<int> indexee par lambdas (approche implicite) 3. Comprendre le mécanisme de capture de closure en C# et son rôle dans Z3.Linq 4. Ajouter des indices (hints) pour resoudre un puzzle reel

Prerequis

.NET 9.0 Interactive
Avoir suivi le notebook 01_Linq2Z3_Intro
Connaissance de base des expressions lambda et closures en C#

Duree estimee : 40-50 minutes

Ce notebook presente la transition pedagogique cle entre deux approches de modelisation Sudoku avec Z3.Linq :

L’approche explicite : 81 proprietes nommees (Cell11, Cell12, …, Cell99), chacune contrainte individuellement. Verbeuse mais pedagogiquement claire.
Le modèle implicite par arrays : une seule propriete List<int> Cells de 81 éléments, indexes par des expressions lambda avec closures. Compacte, generalisable, et extensible.

Cette transition illustre l’innovation apportee par la branche EPFdevelopment du fork Z3.Linq : la capacite d’utiliser des indexeurs de collection dans les expressions lambda traduites en formules SMT.

Contexte : Le modèle implicite par arrays est la base de tous les notebooks Sudoku avances de cette serie. Le comprendre en profondeur est essentiel pour la suite.

Vue d’ensemble : deux stratégies de modelisation du même Sudoku

flowchart TB
    P["Grille Sudoku 9x9\n(81 cellules)"]
    P --> E["Approche 1 — Théorème explicite"]
    P --> I["Approche 2 — Modèle implicite par arrays"]
    E --> E1["81 proprietes nommees\nCell11, Cell12, ..., Cell99"]
    E1 --> E2["Contraintes ecrites une par une\nverbeux, non generalisable"]
    I --> I1["1 propriete List-Int Cells\nindexee par lambdas + closures"]
    I1 --> I2["Boucles generent les contraintes\ncompact, extensible 16x16"]
    E2 --> Z["Z3.Linq -> formules SMT\nsolveur Z3"]
    I2 --> Z
    Z --> S["Solution (assignation valide)"]
    %% 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 I fill:#c8f7c5,color:#1b5e20
    style I1 fill:#c8f7c5,color:#1b5e20
    style I2 fill:#c8f7c5,color:#1b5e20
    style E fill:#f7e3c5,color:#7a5300

Les deux approches produisent le même résultat, mais le modèle implicite (en vert) est celui qui se generalise — il fonde tous les notebooks Sudoku avances de la serie. L’enjeu pedagogique de ce notebook est la transition de l’une vers l’autre.

Configuration de l’environnement

Chargement du fork Z3.Linq (.deploy/) et des espaces de noms nécessaires pour ce notebook.

#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 fork), Microsoft.Z3, System.Collections.Generic, System.Linq");

Imports OK : Z3.Linq (.deploy fork), Microsoft.Z3, System.Collections.Generic, System.Linq

1. Affichage d’une grille Sudoku

Avant de modeliser le Sudoku, definissons une méthode utilitaire pour afficher une grille a partir d’une liste de 81 entiers. Cette méthode sera reutilisee tout au long du notebook.

Convention : les cellules sont stockees dans un List<int> de taille 81, rangees par ligne. L’index d’une cellule à la position (row, col) est row * 9 + col.

void DisplaySudoku(List<int> cells, string title = "Sudoku") {
    Console.WriteLine($"\n=== {title} ===");
    var lineSep = new string('-', 25);
    Console.WriteLine(lineSep);
    for (int row = 0; row < 9; row++) {
        Console.Write("| ");
        for (int col = 0; col < 9; col++) {
            var val = cells[row * 9 + col];
            Console.Write(val == 0 ? ". " : $"{val} ");
            if ((col + 1) % 3 == 0) Console.Write("| ");
        }
        Console.WriteLine();
        if ((row + 1) % 3 == 0) Console.WriteLine(lineSep);
    }
}

// Test avec une grille vide
var emptyGrid = Enumerable.Repeat(0, 81).ToList();
DisplaySudoku(emptyGrid, "Grille vide (test)");
Console.WriteLine($"Methode DisplaySudoku prete ({emptyGrid.Count} cellules)");


=== Grille vide (test) ===
-------------------------
| . . . | . . . | . . . | 
| . . . | . . . | . . . | 
| . . . | . . . | . . . | 
-------------------------
| . . . | . . . | . . . | 
| . . . | . . . | . . . | 
| . . . | . . . | . . . | 
-------------------------
| . . . | . . . | . . . | 
| . . . | . . . | . . . | 
| . . . | . . . | . . . | 
-------------------------
Methode DisplaySudoku prete (81 cellules)

2. Approche 1 : Théorème explicite (81 proprietes)

L’approche la plus naturelle pour modeliser un Sudoku consiste a declarer 81 proprietes nommees, une par cellule : Cell11, Cell12, …, Cell99.

Principe

Chaque propriete represente un entier que Z3 doit determiner. Les contraintes Sudoku se traduisent alors par : - Domaine : chaque propriete entre 1 et 9 - Lignes : les 9 cellules de chaque ligne sont distinctes - Colonnes : les 9 cellules de chaque colonne sont distinctes - Boites 3x3 : les 9 cellules de chaque sous-grille sont distinctes

Classe du modèle explicite

Voici la classe complete. Remarquez la verbosite : 81 lignes de proprietes, chacune devant etre contrainte individuellement.

public class SudokuTable
{
    // 81 proprietes explicites - verbeux mais pedagogiquement clair
    public int Cell11 { get; set; } public int Cell12 { get; set; } public int Cell13 { get; set; }
    public int Cell14 { get; set; } public int Cell15 { get; set; } public int Cell16 { get; set; }
    public int Cell17 { get; set; } public int Cell18 { get; set; } public int Cell19 { get; set; }
    public int Cell21 { get; set; } public int Cell22 { get; set; } public int Cell23 { get; set; }
    public int Cell24 { get; set; } public int Cell25 { get; set; } public int Cell26 { get; set; }
    public int Cell27 { get; set; } public int Cell28 { get; set; } public int Cell29 { get; set; }
    public int Cell31 { get; set; } public int Cell32 { get; set; } public int Cell33 { get; set; }
    public int Cell34 { get; set; } public int Cell35 { get; set; } public int Cell36 { get; set; }
    public int Cell37 { get; set; } public int Cell38 { get; set; } public int Cell39 { get; set; }
    public int Cell41 { get; set; } public int Cell42 { get; set; } public int Cell43 { get; set; }
    public int Cell44 { get; set; } public int Cell45 { get; set; } public int Cell46 { get; set; }
    public int Cell47 { get; set; } public int Cell48 { get; set; } public int Cell49 { get; set; }
    public int Cell51 { get; set; } public int Cell52 { get; set; } public int Cell53 { get; set; }
    public int Cell54 { get; set; } public int Cell55 { get; set; } public int Cell56 { get; set; }
    public int Cell57 { get; set; } public int Cell58 { get; set; } public int Cell59 { get; set; }
    public int Cell61 { get; set; } public int Cell62 { get; set; } public int Cell63 { get; set; }
    public int Cell64 { get; set; } public int Cell65 { get; set; } public int Cell66 { get; set; }
    public int Cell67 { get; set; } public int Cell68 { get; set; } public int Cell69 { get; set; }
    public int Cell71 { get; set; } public int Cell72 { get; set; } public int Cell73 { get; set; }
    public int Cell74 { get; set; } public int Cell75 { get; set; } public int Cell76 { get; set; }
    public int Cell77 { get; set; } public int Cell78 { get; set; } public int Cell79 { get; set; }
    public int Cell81 { get; set; } public int Cell82 { get; set; } public int Cell83 { get; set; }
    public int Cell84 { get; set; } public int Cell85 { get; set; } public int Cell86 { get; set; }
    public int Cell87 { get; set; } public int Cell88 { get; set; } public int Cell89 { get; set; }
    public int Cell91 { get; set; } public int Cell92 { get; set; } public int Cell93 { get; set; }
    public int Cell94 { get; set; } public int Cell95 { get; set; } public int Cell96 { get; set; }
    public int Cell97 { get; set; } public int Cell98 { get; set; } public int Cell99 { get; set; }
}

Console.WriteLine($"Classe SudokuTable definie : 81 proprietes (Cell11..Cell99)");

Classe SudokuTable definie : 81 proprietes (Cell11..Cell99)

Demonstration de l’approche explicite

Pour construire un théorème Sudoku avec ce modèle, il faut enumerer explicitement chaque cellule dans chaque contrainte. Voici un extrait montrant la structure (seule la ligne 1 et la boite haut-gauche sont illustrees pour la lisibilite).

var ctx = new Z3Context();
var theorem = ctx.NewTheorem<SudokuTable>();

// Extrait : contrainte de domaine sur la ligne 1 (9 des 81 necessaires)
theorem = theorem.Where(t => t.Cell11 >= 1 && t.Cell11 <= 9);
theorem = theorem.Where(t => t.Cell12 >= 1 && t.Cell12 <= 9);
theorem = theorem.Where(t => t.Cell13 >= 1 && t.Cell13 <= 9);
theorem = theorem.Where(t => t.Cell14 >= 1 && t.Cell14 <= 9);
theorem = theorem.Where(t => t.Cell15 >= 1 && t.Cell15 <= 9);
theorem = theorem.Where(t => t.Cell16 >= 1 && t.Cell16 <= 9);
theorem = theorem.Where(t => t.Cell17 >= 1 && t.Cell17 <= 9);
theorem = theorem.Where(t => t.Cell18 >= 1 && t.Cell18 <= 9);
theorem = theorem.Where(t => t.Cell19 >= 1 && t.Cell19 <= 9);
// ... 72 contraintes de domaine supplementaires pour les lignes 2 a 9

// Contrainte de ligne 1 : les 9 cellules sont distinctes
theorem = theorem.Where(t => Z3Methods.Distinct(
    t.Cell11, t.Cell12, t.Cell13, t.Cell14, t.Cell15,
    t.Cell16, t.Cell17, t.Cell18, t.Cell19));
// ... 8 contraintes de ligne supplementaires

// Contrainte de boite haut-gauche (3x3)
theorem = theorem.Where(t => Z3Methods.Distinct(
    t.Cell11, t.Cell12, t.Cell13,
    t.Cell21, t.Cell22, t.Cell23,
    t.Cell31, t.Cell32, t.Cell33));
// ... 8 contraintes de boite supplementaires

Console.WriteLine("Approche explicite : chaque contrainte enumere les cellules par leur nom.");
Console.WriteLine("Pour un Sudoku complet, il faut 81 + 9 + 9 + 9 = 108 contraintes explicites.");
Console.WriteLine("(Ici, seules 11 contraintes sont posees pour illustration.");
Console.WriteLine(" Ce theoreme partiel ne produit PAS une solution Sudoku valide.)");

Approche explicite : chaque contrainte enumere les cellules par leur nom.
Pour un Sudoku complet, il faut 81 + 9 + 9 + 9 = 108 contraintes explicites.
(Ici, seules 11 contraintes sont posees pour illustration.
 Ce theoreme partiel ne produit PAS une solution Sudoku valide.)

Limites de l’approche explicite

Aspect	Problème
Verbosite	81 proprietes + 108 contraintes a ecrire à la main
Erreur-prone	Facile d’oublier ou de dupliquer une cellule dans une contrainte
Non generalisable	Impossible d’adapter a un Sudoku 16x16 sans tout reecrire
Maintenance	Ajouter un indice (hint) necessite de connaitre le nom exact de la propriete
Lisibilite	Les contraintes de boite sont illisibles (9 noms de proprietes melanges)

Conclusion : l’approche explicite est pedagogiquement utile pour comprendre ce que Z3 fait, mais elle ne passe pas a l’echelle. C’est ce qui motive le modèle implicite par arrays.

3. Approche 2 : Modèle implicite par arrays

L’approche par arrays exploite une capacite fondamentale de Z3.Linq : la traduction d’indexeurs de collection (list[i]) en variables de decision SMT. Au lieu de 81 proprietes nommees, on utilise une seule propriete List<int> Cells de taille 81.

Principe cle : closures et capture de variable

Quand on ecrit une boucle for qui genere des contraintes Z3 :

for (int i = 0; i < 9; i++) {
    var i1 = i;  // Copie locale OBLIGATOIRE
    theorem = theorem.Where(s => s.Cells[i1 * 9 + j1] > 0);
}

La variable i1 est une copie locale qui capture la valeur de i a chaque itération. Sans cette copie, toutes les expressions lambda partageraient la même reference vers i, qui vaudrait 9 en sortie de boucle. C’est le mécanisme standard de closure en C#, applique ici aux expressions traduites en SMT.

Classe du modèle implicite

public class SudokuArray
{
    public List<int> Cells { get; set; } = Enumerable.Repeat(0, 81).ToList();
}

Console.WriteLine("Classe SudokuArray definie : 1 propriete Cells (List<int> de 81 elements)");

Classe SudokuArray definie : 1 propriete Cells (List<int> de 81 elements)

Construction du théorème avec boucles et closures

Le théorème se construit en trois étapes, chacune utilisant des boucles for au lieu d’enumerations explicites :

Contraintes de domaine : chaque cellule entre 1 et 9
Contraintes structurelles : lignes, colonnes, boites (27 contraintes au total)
Contraintes d’indices : les cellules pre-remplies du puzzle sont fixees

Point cle a observer : la variable var i1 = i; dans chaque boucle. C’est la capture de closure. Sans elle, toutes les expressions lambda referenceraient la même variable i (qui vaudrait sa valeur finale en sortie de boucle), et Z3 resoudrait un problème incorrect.

var ctx2 = new Z3Context();
var theorem2 = ctx2.NewTheorem<SudokuArray>();
var indices = Enumerable.Range(0, 9).ToArray();

// --- Etape 1 : Contraintes de domaine (1..9) ---
for (int i = 0; i < 9; i++) {
    for (int j = 0; j < 9; j++) {
        var i1 = i;  // Capture de closure : copie locale obligatoire
        var j1 = j;
        theorem2 = theorem2.Where(s => s.Cells[i1 * 9 + j1] > 0 && s.Cells[i1 * 9 + j1] < 10);
    }
}

// --- Etape 2a : Contraintes de lignes (9 contraintes) ---
for (int r = 0; r < 9; r++) {
    var r1 = r;
    theorem2 = theorem2.Where(t => Z3Methods.Distinct(
        indices.Select(j => t.Cells[r1 * 9 + j]).ToArray()));
}

// --- Etape 2b : Contraintes de colonnes (9 contraintes) ---
for (int c = 0; c < 9; c++) {
    var c1 = c;
    theorem2 = theorem2.Where(t => Z3Methods.Distinct(
        indices.Select(i => t.Cells[i * 9 + c1]).ToArray()));
}

// --- Etape 2c : Contraintes de boites 3x3 (9 contraintes) ---
for (int b = 0; b < 9; b++) {
    var b1 = b;
    var iStart = b1 / 3;
    var jStart = b1 % 3;
    var idx = iStart * 3 * 9 + jStart * 3;
    theorem2 = theorem2.Where(t => Z3Methods.Distinct(new int[] {
        t.Cells[idx],      t.Cells[idx + 1],  t.Cells[idx + 2],
        t.Cells[idx + 9],  t.Cells[idx + 10], t.Cells[idx + 11],
        t.Cells[idx + 18], t.Cells[idx + 19], t.Cells[idx + 20]
    }));
}

Console.WriteLine($"Modele implicite : 81 contraintes de domaine + 27 contraintes structurelles");
Console.WriteLine($"Le code est 3x plus court et generalisable a toute taille N^2 x N^2.");

Modele implicite : 81 contraintes de domaine + 27 contraintes structurelles
Le code est 3x plus court et generalisable a toute taille N^2 x N^2.

Interprétation — La contrainte AllDifferent

Les trois familles de contraintes structurelles (lignes, colonnes, boîtes) reposent toutes sur la même primitive SMT : Z3Methods.Distinct(...). En programmation par contraintes, cette contrainte porte un nom canonique — AllDifferent — qui exprime que toutes les valeurs d’un ensemble doivent être deux à deux distinctes. C’est l’élément central de tout puzzle Sudoku : chaque ligne, colonne et boîte 3×3 est une instance d’AllDifferent sur 9 variables.

Décomposition de AllDifferent. Une contrainte AllDifferent(x₁, …, xₙ) se décompose canoniquement en inégalités pairwise :

\[ \forall\, i < j,\;\; x_i \neq x_j \]

Pour n = 9, cela fait n·(n−1)/2 = 36 clauses binaires par contrainte (et autant par ligne, colonne, boîte) — une croissance en O(n²). C’est pourquoi AllDifferent est exposé comme une primitive globale (un seul appel Distinct) plutôt qu’à énumérer à la main : le solveur peut alors appliquer des propagations spécialisées (par ex. bound consistency sur le domaine des valeurs) bien plus efficaces que sur 36 clauses ≠ isolées. Z3Methods.Distinct n’est donc pas du sucre syntaxique anodin — c’est un raccourci vers une structure de décision exploitée par le solveur.

Pour aller plus loin : la contrainte AllDifferent et ses encodages alternatifs (pairwise, channeling, propagateurs dédiés) sont un sujet central de la programmation par contraintes (réf. : Handbook of Constraint Programming, Rossi et al., 2006, chap. 6).

Résolution du Sudoku vide

Sans aucune contrainte d’indice, le solveur trouve une solution valide parmi l’ensemble des Sudoku possibles.

var sw = System.Diagnostics.Stopwatch.StartNew();
var solution = theorem2.Solve();
sw.Stop();

Console.WriteLine($"Resolution en {sw.ElapsedMilliseconds} ms");
DisplaySudoku(solution.Cells, "Solution Sudoku (sans indices)");

Resolution en 172363 ms

=== Solution Sudoku (sans indices) ===
-------------------------
| 4 9 1 | 6 7 8 | 5 3 2 | 
| 5 6 8 | 2 3 1 | 7 9 4 | 
| 7 2 3 | 4 9 5 | 1 6 8 | 
-------------------------
| 9 4 2 | 1 6 7 | 3 8 5 | 
| 8 3 5 | 9 2 4 | 6 1 7 | 
| 6 1 7 | 5 8 3 | 4 2 9 | 
-------------------------
| 3 7 9 | 8 4 6 | 2 5 1 | 
| 1 8 6 | 7 5 2 | 9 4 3 | 
| 2 5 4 | 3 1 9 | 8 7 6 | 
-------------------------

Interpretation : Sudoku vide

Le solveur produit une grille Sudoku valide (chaque ligne, colonne et boite 3x3 contient les chiffres 1 a 9 exactement une fois). Ce n’est pas un Sudoku “interessant” (pas de puzzle a resoudre), mais il demontre que toutes les contraintes structurelles sont correctes.

Aspect	Valeur	Signification
Contraintes de domaine	81	Chaque cellule dans [1, 9]
Contraintes de lignes	9	Une par ligne
Contraintes de colonnes	9	Une par colonne
Contraintes de boites	9	Une par boite 3x3
Total	108	Identique a l’approche explicite, mais genere par boucles

Note technique : le modèle implicite genere exactement le même ensemble de contraintes SMT que le modèle explicite. La différence est purement syntaxique (C#), pas sémantique (Z3).

Précision de vocabulaire — « array » C# vs « Array » SMT

Puisque nous venons d’évoquer le niveau SMT, il faut clarifier un point de vocabulaire qui sinon prête à confusion : le mot « array » dans ce notebook ne désigne pas la théorie des tableaux de Z3.

Ici, « array » = List<int> C#. La propriété Cells est une collection C#, et l’indexeur s.Cells[i*9+j] est un sucre d’indexeur que Z3.Linq traduit en une variable de décision Z3 distincte par cellule (81 variables au total, comme le rappelle la conclusion). Le « modèle implicite par arrays » compactifie donc le code source C#, pas la représentation SMT — d’où la note ci-dessus : les deux approches génèrent le même ensemble de contraintes.
La théorie des tableaux SMT (le (Array Int Int) de SMT-LIB, avec ses opérations select/store et les axiomes de McCarthy) est autre chose : là, le tableau est un seul symbole logique que l’on interroge par select(arr, i). Cette théorie est enseignée dans le notebook 04 — Array Theory.

Le « array » de ce notebook et l’« Array » de NB-04 sont donc deux notions différentes qui partagent un mot. Si vous cherchez à modéliser le Sudoku comme un vrai tableau SMT (select/store), c’est NB-04 qu’il faut voir ; la comparaison des deux modes d’encodage des collections (une variable par cellule vs un seul symbole de tableau) est elle détaillée dans le notebook 03 — Sudoku Modes Comparison.

4. Résolution avec un puzzle reel (indices)

La vraie puissance du modèle implicite apparait quand on ajoute des indices (cellules pre-remplies du puzzle). Avec l’approche explicite, ajouter un indice suppose connaitre le nom de la propriete (Cell34). Avec le modèle implicite, une simple boucle suffit.

Puzzle classique

Nous utilisons un puzzle Sudoku classique ou 0 represente une cellule vide.

// Un puzzle Sudoku classique (0 = cellule vide)
var puzzle = new SudokuArray {
    Cells = new List<int> {
        5,3,0, 0,7,0, 0,0,0,
        6,0,0, 1,9,5, 0,0,0,
        0,9,8, 0,0,0, 0,6,0,
        8,0,0, 0,6,0, 0,0,3,
        4,0,0, 8,0,3, 0,0,1,
        7,0,0, 0,2,0, 0,0,6,
        0,6,0, 0,0,0, 2,8,0,
        0,0,0, 4,1,9, 0,0,5,
        0,0,0, 0,8,0, 0,7,9
    }
};

int givenCount = puzzle.Cells.Count(c => c != 0);
Console.WriteLine($"Puzzle charge : {givenCount} indices sur 81 cellules");
DisplaySudoku(puzzle.Cells, "Puzzle initial");

Puzzle charge : 30 indices sur 81 cellules

=== Puzzle initial ===
-------------------------
| 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 | 
-------------------------

Construction du théorème avec indices

Le théorème combine les mêmes contraintes structurelles que precedemment, plus une contrainte par cellule pre-remplie. Remarquez la troisieme boucle for : elle parcourt les 81 cellules et fixe uniquement les valeurs non-nulles.

var ctx3 = new Z3Context();
var puzzleTheorem = ctx3.NewTheorem<SudokuArray>();

// --- Contraintes de domaine (1..9) ---
for (int i = 0; i < 9; i++) {
    for (int j = 0; j < 9; j++) {
        var i1 = i; var j1 = j;
        puzzleTheorem = puzzleTheorem.Where(s => s.Cells[i1 * 9 + j1] > 0 && s.Cells[i1 * 9 + j1] < 10);
    }
}

// --- Contraintes de lignes ---
for (int r = 0; r < 9; r++) {
    var r1 = r;
    puzzleTheorem = puzzleTheorem.Where(t => Z3Methods.Distinct(
        indices.Select(j => t.Cells[r1 * 9 + j]).ToArray()));
}

// --- Contraintes de colonnes ---
for (int c = 0; c < 9; c++) {
    var c1 = c;
    puzzleTheorem = puzzleTheorem.Where(t => Z3Methods.Distinct(
        indices.Select(i => t.Cells[i * 9 + c1]).ToArray()));
}

// --- Contraintes de boites 3x3 ---
for (int b = 0; b < 9; b++) {
    var b1 = b;
    var iStart = b1 / 3; var jStart = b1 % 3;
    var idx = iStart * 3 * 9 + jStart * 3;
    puzzleTheorem = puzzleTheorem.Where(t => Z3Methods.Distinct(new int[] {
        t.Cells[idx],      t.Cells[idx + 1],  t.Cells[idx + 2],
        t.Cells[idx + 9],  t.Cells[idx + 10], t.Cells[idx + 11],
        t.Cells[idx + 18], t.Cells[idx + 19], t.Cells[idx + 20]
    }));
}

// --- Contraintes d'indices : fixer les cellules pre-remplies ---
int hintCount = 0;
for (int i = 0; i < 81; i++) {
    if (puzzle.Cells[i] != 0) {
        var idx = i;
        var val = puzzle.Cells[i];
        puzzleTheorem = puzzleTheorem.Where(s => s.Cells[idx] == val);
        hintCount++;
    }
}

Console.WriteLine($"Theoreme construit : 108 contraintes structurelles + {hintCount} contraintes d'indices");

Theoreme construit : 108 contraintes structurelles + 30 contraintes d'indices

Résolution du puzzle

Le théorème est complet (contraintes structurelles + indices). Lancons la résolution.

sw.Restart();
var solved = puzzleTheorem.Solve();
sw.Stop();
DisplaySudoku(solved.Cells, $"Solution (en {sw.ElapsedMilliseconds} ms)");


=== Solution (en 88 ms) ===
-------------------------
| 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 | 
-------------------------

Interpretation : puzzle resolu

Le solveur Z3 trouve la solution unique du puzzle en quelques millisecondes. Chaque cellule vide a ete completee de maniere a satisfaire toutes les contraintes.

Aspect	Valeur	Signification
Cellules pre-remplies	30	Données du puzzle
Cellules a determiner	51	Trouvees par Z3
Temps de résolution	variable	Généralement < 100 ms
Solutions possibles	1	Le puzzle a une solution unique

Note : le modèle implicite rend l’ajout d’indices trivial (une boucle). Avec l’approche explicite, il faudrait ecrire 30 contraintes individuelles Where(t => t.CellXY == val), en connaissant le mapping position -> nom de propriete.

5. Tableau comparatif des deux approches

Aspect	Approche explicite (81 proprietes)	Modèle implicite (List)
Nombre de proprietes	81 (Cell11…Cell99)	1 (Cells)
Contraintes de domaine	81 expressions `Where(t => t.CellXY >= 1)`	Boucle `for` 81 itérations
Contraintes de ligne	9 lambdas enumerant 9 cellules chacune	1 boucle `for` avec `Z3Methods.Distinct`
Contraintes de boite	9 lambdas enumerant 9 cellules chacune	1 boucle `for` avec arithmetique d’index
Ajout d’indices	Copier-coller + edition manuelle	Boucle sur les cellules non-nulles
Generalisable a N^2	Non (taille fixe)	Oui (boucles parametriques)
Capture de closure	Non applicable	`var i1 = i;` indispensable
Code total (lignes)	~200+	~50

Conclusion : le modèle implicite par arrays est superieur sur tous les plans, sauf la transparence initiale. L’approche explicite reste utile comme étape pedagogique pour comprendre que Z3 créé bien une variable de decision par cellule.

6. Exercice 1 : Sudoku 16x16

Adaptez le modèle implicite pour un Sudoku 16x16 : - Cells contient 256 éléments (16x16) - Domaine : chaque cellule entre 1 et 16 - Rangees : 16 contraintes de 16 valeurs distinctes - Colonnes : 16 contraintes de 16 valeurs distinctes - Boites : 16 boites de taille 4x4

Indices : - Modifier les boucles pour n = 16 et blockSize = 4 - L’arithmetique d’index pour les boites utilise b / 4 et b % 4 (au lieu de b / 3 et b % 3) - L’offset entre lignes dans une boite passe de 9 a 16

// Exercice : adapter le modele implicite pour un Sudoku 16x16
// - Cells contient 256 elements (16x16)
// - Domaine : chaque cellule entre 1 et 16
// - Rangees : 16 contraintes de 16 valeurs distinctes
// - Colonnes : 16 contraintes de 16 valeurs distinctes
// - Boites : 16 boites 4x4
// Indice : modifier les boucles pour n=16 et blockSize=4
// L'offset entre lignes dans une boite passe de 9 a 16

// TODO etudiant : implementer le theoreme pour Sudoku16
// public class Sudoku16Array { public List<int> Cells { get; set; } = ...; }
// var ctx16 = new Z3Context();
// var theorem16 = ctx16.NewTheorem<Sudoku16Array>();
// ... contraintes de domaine, lignes, colonnes, boites ...
// var solution16 = theorem16.Solve();

Console.WriteLine("Exercice a completer : Sudoku 16x16");

Exercice a completer : Sudoku 16x16

7. Exercice 2 : Mesurer le temps de résolution en fonction de la difficulte

Generez des puzzles avec un nombre variable d’indices (de 17, le minimum théorique, a 40) et mesurez le temps de résolution par Z3.

Objectif : comprendre comment la difficulte du puzzle (nombre d’indices) influence le temps de résolution.

Indices : - Partir d’une solution complete ( utilisez le théorème sans indices) - Supprimer progressivement des cellules aleatoirement pour créer des puzzles de difficulte croissante - Chronometrer theorem.Solve() pour chaque puzzle - Afficher un tableau recapitulatif : nombre d’indices | temps (ms) | statut

// Exercice : mesurer le temps de resolution pour des puzzles de difficulte croissante
// 1. Partir d'une solution complete (theoreme sans indices)
// 2. Supprimer progressivement des cellules (ou utiliser des puzzles connus)
// 3. Chronometrer theorem.Solve() pour chaque niveau
// 4. Afficher un tableau resultat : indices | temps (ms) | statut

// Indice : utiliser Random pour selectionner les cellules a supprimer
// var rng = new Random(42);
// var cellsToRemove = Enumerable.Range(0, 81).OrderBy(_ => rng.Next()).Take(n).ToList();

// TODO etudiant : implementer le benchmark
Console.WriteLine("Exercice a completer : benchmark difficulte");

Exercice a completer : benchmark difficulte

8. Exercice 3 : Generer plusieurs solutions

Un Sudoku bien pose a une solution unique. Mais si le puzzle est sous-contraint (trop peu d’indices), il peut avoir plusieurs solutions. Le but de cet exercice est de trouver et denombrer ces solutions.

Objectif : modifier le théorème pour trouver plusieurs solutions distinctes et verifier l’ununicite.

Indices : - Resoudre le puzzle une première fois - Ajouter une contrainte excluant la solution trouvee : au moins une cellule doit differer - Re-resoudre pour trouver la solution suivante - Repeter jusqu’a ce qu’il n’y ait plus de solution - Pour exclure : Where(s => s.Cells[0] != sol.Cells[0] || s.Cells[1] != sol.Cells[1] || ...)

// Exercice : trouver toutes les solutions d'un puzzle incomplet
// 1. Resoudre le puzzle
// 2. Ajouter une contrainte excluant la solution trouvee
// 3. Re-resoudre pour trouver la solution suivante
// 4. Compter le nombre de solutions
// Indice : exclure = Where(s => s.Cells[0] != solution.Cells[0] || s.Cells[1] != solution.Cells[1] || ...)

// TODO etudiant : implementer la recherche multi-solutions
Console.WriteLine("Exercice a completer : solutions multiples");

Exercice a completer : solutions multiples

B8 - Quantificateurs bornes (DSL `Z3Methods.ForAll` / `Exists`)

La section 3 de ce notebook deroule à la main les contraintes de cellule : une boucle C# emet une propriete par index (« chaque cellule dans [1,9] », les lignes/colonnes/blocs Distinct). C’est le pain quotidien de la modelisation par tableau - mais la boucle grandit avec la taille et melange la logique du modèle et la mecanique du deroulage. Le binding ajoute deux quantificateurs bornes : Z3Methods.ForAll(domaine, i => predicat) et Z3Methods.Exists(domaine, i => predicat). Le domaine est evalue dans l’hote (un IEnumerable C#) et le predicat est deroule en une conjonction (ForAll -> MkAnd) ou une disjonction (Exists -> MkOr) sur chaque élément. Une seule .Where(...) exprime alors ce qui exigeait une boucle emettant un .Where par index. Ce sont des quantificateurs finis : pas les quantificateurs SMT sur un sort non borne (MkForall), mais un deroulage statique sur un index enumerable.

Stack : A + B - pourquoi. On modelise une rangee de 4 cellules (un mini-Sudoku 1D), palette {1,2,3,4}. Deux contraintes quantifiees : universelle « chaque cellule dans [1,4] » et existentielle « au moins une cellule vaut 4 » (le maximum apparait). Cote raw, on deroule à la main : une boucle construit la conjonction MkAnd des bornes et une autre la disjonction MkOr des egalites a 4. Cote DSL, les mêmes quantificateurs s’ecrivent en une ligne : Z3Methods.ForAll(Enumerable.Range(0, N), i => ...) et Z3Methods.Exists(...). Le contraste : le système est SAT avec témoin ; puis, en reduisant les bornes a [1,3], « une cellule vaut 4 » devient UNSAT (aucun 4 possible sous 3) - obtenu des deux cotes sur le même modèle.

// B8 - Quantificateurs bornes "ForAll/Exists" : deux stacks sur une MEME rangee de cellules.
//   Une rangee de 4 cellules (mini-Sudoku 1D). Palette : {1,2,3,4}.
//   Universel : chaque cellule dans [1,4].   Existentiel : au moins une cellule vaut 4 (le max apparait).
//   SAT -> temoin ; puis bornes reduites a [1,3] + "une cellule vaut 4" -> UNSAT (aucun 4 possible sous 3).
const int N = 4;

// Classe au niveau cellule (requise par NewTheorem<T>) : une rangee de cellules.
public class Row { public int[] Cells { get; set; } = new int[N]; }

// =====================================================================
// BLOC RAW (API brute Microsoft.Z3) : universel/existentiel deroules a la main en MkAnd/MkOr
// =====================================================================
{
    using var z3 = new Microsoft.Z3.Context();
    IntExpr[] v = new IntExpr[N];
    for (int i = 0; i < N; i++) v[i] = z3.MkIntConst($"c{i}");

    // Universel : chaque cellule dans [1,4], DEROULE a la main en conjonction (une contrainte par index)
    var bounds = new System.Collections.Generic.List<Microsoft.Z3.BoolExpr>();
    for (int i = 0; i < N; i++) bounds.Add(z3.MkAnd(z3.MkGe(v[i], z3.MkInt(1)), z3.MkLe(v[i], z3.MkInt(4))));
    Microsoft.Z3.BoolExpr forall14 = z3.MkAnd(bounds.ToArray());

    // Existentiel : au moins une cellule vaut 4, DEROULE a la main en disjonction
    var disj = new System.Collections.Generic.List<Microsoft.Z3.BoolExpr>();
    for (int i = 0; i < N; i++) disj.Add(z3.MkEq(v[i], z3.MkInt(4)));
    Microsoft.Z3.BoolExpr existsMax = z3.MkOr(disj.ToArray());

    var sSat = z3.MkSolver();
    sSat.Assert(forall14);
    sSat.Assert(existsMax);
    Status stSat = sSat.Check();
    Console.WriteLine($"[RAW] ForAll(c dans [1,4]) & Exists(c==4) : {stSat}");
    if (stSat == Status.SATISFIABLE) {
        var m = sSat.Model;
        var sb = new System.Text.StringBuilder();
        for (int i = 0; i < N; i++) { if (i > 0) sb.Append(","); sb.Append(m.Eval(v[i], true)); }
        Console.WriteLine($"[RAW]   temoin : [{sb}]");
    }

    // Bornes reduites a [1,3] : "une cellule vaut 4" devient impossible -> UNSAT
    var bounds13 = new System.Collections.Generic.List<Microsoft.Z3.BoolExpr>();
    for (int i = 0; i < N; i++) bounds13.Add(z3.MkAnd(z3.MkGe(v[i], z3.MkInt(1)), z3.MkLe(v[i], z3.MkInt(3))));
    var sUn = z3.MkSolver();
    sUn.Assert(z3.MkAnd(bounds13.ToArray()));
    sUn.Assert(existsMax);
    Console.WriteLine($"[RAW] ForAll(c dans [1,3]) & Exists(c==4) : {sUn.Check()}   (aucun 4 possible sous 3)");
}

// =====================================================================
// BLOC DSL (Z3.Linq) : le meme universel/existentiel en une ligne sur Enumerable.Range
// =====================================================================
{
    using var thCtx = new Z3Context();

    var sat = thCtx.NewTheorem<Row>()
        .Where(e => Z3Methods.ForAll(Enumerable.Range(0, N), i => e.Cells[i] >= 1 && e.Cells[i] <= 4))
        .Where(e => Z3Methods.Exists(Enumerable.Range(0, N), i => e.Cells[i] == 4))
        .Solve();
    if (sat != null)
        Console.WriteLine($"[DSL] ForAll(c dans [1,4]) & Exists(c==4) : SAT  -> [{string.Join(",", sat.Cells)}]");

    var unsat = thCtx.NewTheorem<Row>()
        .Where(e => Z3Methods.ForAll(Enumerable.Range(0, N), i => e.Cells[i] >= 1 && e.Cells[i] <= 3))
        .Where(e => Z3Methods.Exists(Enumerable.Range(0, N), i => e.Cells[i] == 4))
        .Solve();
    Console.WriteLine($"[DSL] ForAll(c dans [1,3]) & Exists(c==4) : {(unsat == null ? "UNSAT" : "SAT?!")}   (le quantificateur borne se contredit)");

    // Semantique du domaine vide : ForAll vide = vrai (vacuite), Exists vide = faux
    var vac = thCtx.NewTheorem<Row>()
        .Where(e => Z3Methods.ForAll(Enumerable.Empty<int>(), i => e.Cells[i] > e.Cells[i]))  // predicat faux, mais domaine vide
        .Where(e => e.Cells[0] == 2)
        .Solve();
    Console.WriteLine($"[DSL] ForAll(domaine vide, predicat faux) : {(vac == null ? "UNSAT" : "SAT")}   (universel vide = vrai par vacuite)");
}

[RAW] ForAll(c dans [1,4]) & Exists(c==4) : SATISFIABLE
[RAW]   temoin : [4,1,1,1]
[RAW] ForAll(c dans [1,3]) & Exists(c==4) : UNSATISFIABLE   (aucun 4 possible sous 3)
[DSL] ForAll(c dans [1,4]) & Exists(c==4) : SAT  -> [4,3,1,2]
[DSL] ForAll(c dans [1,3]) & Exists(c==4) : UNSAT   (le quantificateur borne se contredit)
[DSL] ForAll(domaine vide, predicat faux) : SAT   (universel vide = vrai par vacuite)

Lecture B8 - deux ecritures d’un quantificateur borne, un même deroulage

Les deux stacks contraignent la même rangee avec les mêmes quantificateurs - universel « tout dans [1,4] », existentiel « un 4 apparait » - et donnent les mêmes verdicts : SAT avec témoin, puis UNSAT des que les bornes tombent a [1,3]. La différence est comment on ecrit le deroulage :

Aspect	RAW (boucle + `MkAnd`/`MkOr`)	DSL (`ForAll`/`Exists` sur `Range`)
Universel	boucle C# -> `MkAnd(bounds.ToArray())`	`Z3Methods.ForAll(Enumerable.Range(0, N), i => ...)`
Existentiel	boucle C# -> `MkOr(disj.ToArray())`	`Z3Methods.Exists(Enumerable.Range(0, N), i => ...)`
Taille du code	croit avec le nombre d’index (une boucle explicite)	constante : une `.Where` quel que soit `N`
Domaine vide	a gerer soi-même	`ForAll` vide = vrai, `Exists` vide = faux (vacuite classique)

Ligne de contraste (a retenir) : le raw materialise le deroulage - une boucle C# assemble la conjonction (MkAnd) ou la disjonction (MkOr) index par index ; le DSL le declare - ForAll/Exists sur un Enumerable.Range deroulent en interne vers exactement le même MkAnd/MkOr. Même deroulage, même verdict, mais la logique du modèle ne se noie plus dans la mecanique de la boucle. Attention : ce sont des quantificateurs finis (le domaine est un IEnumerable C# evalue dans l’hote), pas les quantificateurs SMT sur un sort non borne.

Cas d’usage : les quantificateurs bornes sont l’idiome des grilles et tableaux - rangees de Sudoku, N-reines, fenêtres d’ordonnancement - partout ou une contrainte s’applique « pour tout / il existe » sur un index enumerable. Ils remplacent la boucle emettant un .Where par index (section 3 de ce notebook). On garde le deroulage manuel quand le domaine n’est pas statiquement enumerable (il depend du modèle) ou quand il faut un vrai quantificateur SMT non borne (MkForall/MkExists), hors de portee du deroulage fini.

Conclusion

Ce notebook a illustre la transition fondamentale entre deux paradigmes de modelisation Sudoku avec Z3.Linq :

Recapitulatif

Concept	Point cle
Théorème explicite	81 proprietes nommees, chaque contrainte enumere les cellules
Modèle implicite	1 `List<int>` indexee, boucles generent les contraintes
Capture de closure	`var i1 = i;` est obligatoire pour capturer la valeur de boucle
Arithmetique d’index	`row * 9 + col` pour l’index lineaire, `b / 3` et `b % 3` pour les boites
Ajout d’indices	Boucle sur les cellules non-nulles, une contrainte `Where` par indice

Pour aller plus loin

Sudoku 16x16 (Exercice 1) : la generalisation demontre la puissance du modèle implicite
Benchmark difficulte (Exercice 2) : comprendre la complexite algorithmique du solveur
Solutions multiples (Exercice 3) : vérification d’universalite et denomination

Dans les notebooks suivants de la serie Z3, le modèle implicite par arrays sera la base de toutes les modelisations avancees.

Navigation : << Introduction Linq2Z3 | Serie Z3 | Index SymbolicAI

Retour au sommet