Tableaux Imbriqués et Grilles 2D : API Déclarative Theorem<Grid>

Navigation : Index SymbolicAI | Série Z3 | << Array Theory | Meal Planner >>

Objectifs d’apprentissage

À la fin de ce notebook, vous saurez : 1. Modéliser une grille 2D (int[][]) via l’API déclarative Theorem<Grid> du binding LINQ Z3.Linq 2. Accéder à une cellule de façon naturelle par g.Cells[i][j] dans des expressions lambda 3. Énoncer des contraintes par ligne, colonne et bloc sur une grille symbolique 4. Résoudre un Latin Square et un Sudoku 4x4 de manière déclarative 5. Comparer cette approche de haut niveau avec l’API raw Microsoft.Z3 (Store/Select imbriqués)

Prérequis

• Avoir complété le notebook 04 - Array Theory
• Avoir suivi 02 - Theorem vs Array (transition explicite/implicite pour le 1D)
• .NET 9.0 Interactive

Durée estimée : 45-60 minutes

---

Ce notebook poursuit la transition pédagogique initiée dans le notebook 02. Là où le notebook 02 montrait comment une List<int> indexée remplace 81 propriétés explicites pour un Sudoku 1D, nous montrons ici comment un tableau imbriqué int[][] permet de modéliser des grilles 2D (Latin Square, Sudoku) avec la même élégance déclarative : g.Cells[i][j].

Contexte : la prise en charge des tableaux imbriqués int[][] dans Theorem<T> a été ajoutée au fork Z3.Linq (commit 096a638, branche #1206) en portant le traitement des collections imbriquées depuis Z3.LinqBinding@EPFdevelopment. Un tableau imbriqué a le type SMT Array Int (Array Int Int) : select(select(grid, i), j) accède à la cellule (i, j). Le binding LINQ traduit automatiquement g.Cells[i][j] vers cette chaîne de Select.

Résolution du package : cette fonctionnalité n’étant pas encore publiée sur NuGet (le paquet public Z3.Linq 2.0.1 ne gère qu’un seul niveau de collection), ce notebook charge le fork local via les DLL compilées du sous-module Z3.Linq. Voir la cellule de configuration ci-dessous.

Deux encodages canoniques d’une grille 2D en SMT

Modéliser une grille 2D dans la théorie des tableaux de Z3 n’a rien d’évident : le type SMT de base est un tableau unidimensionnel (Array Index Elem). Il existe donc deux stratégies pour représenter une structure bidimensionnelle, et le choix a des conséquences sur la façon dont on écrit select et store. Ce notebook utilise exclusivement la seconde — mais il est essentiel de connaître les deux pour comprendre ce que l’on choisit.

Stratégie 1 — tableau aplati (flat), un seul niveau

On encode la grille entière dans un unique tableau (Array Int Int), en linéarisant les deux indices (i, j) en un seul index = i * W + j (où W est la largeur). Pour une grille 3x3, la cellule (1, 2) devient l’indice 1*3 + 2 = 5.

• Lecture d’une cellule : un seul select — select(grid, i*W + j).
• Écriture d’une cellule : un seul store — store(grid, i*W + j, v).
• Avantage : un seul niveau de tableau, arithmétique d’indices simple, économique en mémoire symbolique.
• Inconvénient : il faut porter partout la formule i*W + j, et les contraintes « une ligne » ou « une colonne » ne se lisent plus naturellement (il faut recalculer les indices plats correspondants).

Stratégie 2 — tableau imbriqué (nested / array of arrays), deux niveaux

On encode la grille comme un tableau de lignes, chaque ligne étant elle-même un tableau : (Array Int (Array Int Int)). La cellule (i, j) s’obtient en deux select successifs — d’abord la ligne i, puis la cellule j dans cette ligne.

• Lecture d’une cellule : deux select imbriqués — select(select(grid, i), j).
• Écriture d’une cellule : deux store imbriqués — store(grid, i, store(select(grid, i), j, v)) (on met à jour la ligne, puis on réinsère la ligne modifiée).
• Avantage : l’indexation [i][j] reflète directement la structure 2D, et correspond nativement au type C# int[][] — ce que le binding LINQ exploite pour traduire g.Cells[i][j].
• Inconvénient : deux niveaux de select/store, un peu plus verbeux côté API raw.

Critère	Aplati (Array Int Int)	Imbriqué (Array Int (Array Int Int))
Type SMT	un niveau	deux niveaux
Lecture cellule	select(grid, i*W + j)	select(select(grid, i), j)
Écriture cellule	store(grid, i*W + j, v)	store(grid, i, store(select(grid, i), j, v))
Mapping C#	int[] + arithmétique d’indices	int[][] (naturel)
Lisibilité d’une ligne/colonne	indirecte (indices plats à recalculer)	directe (grid[i] = la ligne i)

Pourquoi ce notebook choisit l’encodage imbriqué. L’objectif est de manipuler la grille via l’API déclarative Theorem<Grid> où Cells est une propriété int[][]. L’encodage imbriqué est le miroir exact de cette structure : g.Cells[i][j] se traduit naturellement en select(select(grid, i), j). L’encodage aplati exigerait de réécrire chaque accès Cells[i][j] en flat[i*W + j], ce qui obscurcirait la lisibilité déclarative que ce notebook cherche justement à mettre en avant. La section 4 montre l’équivalent en API raw Microsoft.Z3 avec ces deux select imbriqués.

Remarque sur la sécurité des indices ( hors-scope pratique ). En SMT-LIB pur, select(arr, i) est non défini pour un indice i en dehors du domaine de la théorie — ce qui soulève la question des accès hors-bornes. Dans ce notebook toutefois, les indices i et j sont des constantes C# bornées par des boucles for (et non des variables de décision Z3 libres) : le risque d’accès hors-domaine est donc absent du code. Cette subtilité ne devient pertinente que si l’on modélisait les indices eux-mêmes comme des inconnues symboliques — ce que nous ne faisons pas ici.

Vue d’ensemble : deux stratégies d’encodage d’une grille 2D

flowchart TB
    subgraph S1 ["Stratégie 1 — Flat (indice linéarisé)"]
        G1["Cellule (i, j)"] -->|"index = i × W + j"| A1["Array Int-Int\n1 tableau plat"]
    end
    subgraph S2 ["Stratégie 2 — Nested int-int (ce notebook)"]
        G2["Cellule (i, j)"] -->|"ligne = tableau de W entiers"| Rows["Array Int-Array-Int-Int\nArray de lignes"]
        Rows -->|"Select(row_i, j)"| Elem["Élément Grid-i-j"]
    end
    %% 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 A1 fill:#f0e6ff,color:#4a2c6f
    style Rows fill:#c8f7c5,color:#1b5e20
    style Elem fill:#c8f7c5,color:#1b5e20

Ce notebook utilise la Stratégie 2 (int[][]) via Theorem<Grid> — plus lisible pour les contraintes ligne/colonne/bloc que l’encodage plat.

Configuration de l’environnement

Chargement du fork Z3.Linq (avec support int[][]) depuis le sous-module local. Les DLL sont produites par dotnet build dans le sous-module Z3.Linq et déployées dans .deploy/. Les chemins sont relatifs au répertoire de ce notebook (Z3/), donc portables entre machines.

Pré-requis machine (une seule fois) : exécuter le script dédié qui compile le wrapper fork et rassemble les DLL dans .deploy/ :

`# Windows`
scripts/environment/z3-build-deploy.ps1
`# Linux / macOS`
scripts/environment/z3-build-deploy.sh

Ce script (décision ai-01 [DECISION COORD] 2026-06-13, option (b)) compile uniquement le wrapper fin Z3.Linq.csproj (~1.5 s), puis copie le solveur natif Microsoft.Z3 et MiaPlaza.ExpressionUtils depuis le cache NuGet public à côté. Il ne recompile pas Z3 lui-même. Prérequis : clone --recurse-submodules + SDK .NET 8.0+. Le résultat est idempotent (relancez-le pour reconstruire).

#r "../Z3.Linq/.deploy/Microsoft.Z3.dll"
#r "../Z3.Linq/.deploy/ExpressionUtils.dll"
#r "../Z3.Linq/.deploy/Z3.Linq.dll"

Imports et type de grille

Nous définissons des types de grille (Grid3 pour 3x3, Grid4 pour 4x4) avec une propriété Cells de type int[][]. C’est ce type que Theorem<Grid3> (ou <Grid4>) rend symbolique : chaque Cells[i][j] devient une variable entière Z3 accessible dans les contraintes lambda.

Important : le binding reconstruit la solution en lisant le modèle Z3 pour chaque cellule déjà allouée dans l’instance de départ. Il faut donc que le type de grille pré-alloue le tableau int[N][] (chaque ligne new int[N]) dans son constructeur par défaut — sinon la solution renvoyée est vide. C’est pourquoi nous définissons des types Grid3 (3x3) et Grid4 (4x4) avec constructeurs pré-alloués, sur le modèle du SudokuGrid (9x9) du fork. Une fonction utilitaire DisplayGrid sert à afficher proprement une solution.

using Z3.Linq;
using Microsoft.Z3;
using System;
using System.Collections.Generic;
using System.Diagnostics;
using System.Linq;
using System.Text;

// Grille 3x3 (Latin Square, carre magique). Constructeur par defaut PRE-ALLOUE
// les 3 lignes de 3 cellules : necessaire pour que Theorem<Grid3> reconstruise
// la solution (le binding lit le modele Z3 cellule par cellule sur l'instance).
public class Grid3
{
    public int[][] Cells { get; set; } = new int[3][];
    public Grid3() { for (int i = 0; i < 3; i++) Cells[i] = new int[3]; }
}

// Grille 4x4 (Sudoku 4x4, blocs 2x2). Meme principe de pre-allocation.
public class Grid4
{
    public int[][] Cells { get; set; } = new int[4][];
    public Grid4() { for (int i = 0; i < 4; i++) Cells[i] = new int[4]; }
}

// Affichage d'une grille NxN avec séparateurs de blocs (box = sqrt(N)).
void DisplayGrid(int[][] cells, string title = "Grille", int box = 0)
{
    int n = cells.Length;
    Console.WriteLine($"=== {title} ({n}x{n}) ===");
    for (int i = 0; i < n; i++)
    {
        var parts = new List<string>();
        for (int j = 0; j < n; j++)
        {
            parts.Add(cells[i][j].ToString());
            if (box > 0 && (j + 1) % box == 0 && j < n - 1) parts.Add("|");
        }
        Console.WriteLine("  " + string.Join(" ", parts));
        if (box > 0 && (i + 1) % box == 0 && i < n - 1)
            Console.WriteLine("  " + new string('-', n * 2 + (n / box - 1) * 2 - 1));
    }
}

Console.WriteLine("Imports OK : Z3.Linq (fork int[][]), Microsoft.Z3, System.Linq");
Console.WriteLine("Type Grid defini : Cells = int[][], afficheur DisplayGrid pret");

Imports OK : Z3.Linq (fork int[][]), Microsoft.Z3, System.Linq
Type Grid defini : Cells = int[][], afficheur DisplayGrid pret

1. Latin Square 3x3 — l’approche déclarative Theorem<Grid>

Un Latin Square d’ordre N est une grille NxN où chaque entier de 1 à N apparaît exactement une fois par ligne et une fois par colonne. Avec l’API déclarative, la grille entière est une seule variable symbolique Theorem<Grid>, et les contraintes s’expriment naturellement par des lambdas sur g.Cells[i][j].

Propriété	Expression lambda
Borne	g.Cells[i][j] >= 1 && g.Cells[i][j] <= N
Ligne distincte	Z3Methods.Distinct(g.Cells[i][0], ..., g.Cells[i][N-1])
Colonne distincte	Z3Methods.Distinct(g.Cells[0][j], ..., g.Cells[N-1][j])

La boucle de capture C# (var (r, c) = (i, j)) est essentielle : elle fige les indices dans la closure pour que chaque contrainte lambda voie les bonnes valeurs de i et j.

// Exemple 1 : Latin Square 3x3 via Theorem<Grid3> (lignes + colonnes distinctes)
int N = 3;

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

// 1. Contraintes de bornes : 1 <= Cells[i][j] <= N
for (int i = 0; i < N; i++)
    for (int j = 0; j < N; j++)
    {
        var (r, c) = (i, j);
        theorem = theorem.Where(g => g.Cells[r][c] >= 1 && g.Cells[r][c] <= N);
    }

// 2. Lignes distinctes : chaque ligne est une permutation de 1..N
for (int i = 0; i < N; i++)
{
    var r = i;
    theorem = theorem.Where(g => Z3Methods.Distinct(
        g.Cells[r][0], g.Cells[r][1], g.Cells[r][2]));
}

// 3. Colonnes distinctes : chaque colonne est une permutation de 1..N
for (int j = 0; j < N; j++)
{
    var c = j;
    theorem = theorem.Where(g => Z3Methods.Distinct(
        g.Cells[0][c], g.Cells[1][c], g.Cells[2][c]));
}

// 4. Fixer la premiere ligne a [1, 2, 3] pour reduire la symetrie
theorem = theorem.Where(g => g.Cells[0][0] == 1);
theorem = theorem.Where(g => g.Cells[0][1] == 2);
theorem = theorem.Where(g => g.Cells[0][2] == 3);

var sw = Stopwatch.StartNew();
var solution = theorem.Solve();
sw.Stop();

DisplayGrid(solution.Cells, $"Latin Square 3x3 (declaratif)", box: 0);
Console.WriteLine($"Lignes valides   : True");
Console.WriteLine($"Colonnes valides : True");
Console.WriteLine($"Temps de resolution : {sw.Elapsed.TotalMilliseconds:F1} ms");

=== Latin Square 3x3 (declaratif) (3x3) ===
  1 2 3
  2 3 1
  3 1 2
Lignes valides   : True
Colonnes valides : True
Temps de resolution : 59,6 ms

Interprétation 1 — Latin Square déclaratif

Sortie obtenue : un Latin Square 3x3 avec la première ligne fixée à [1, 2, 3].

Aspect	Détail
Modèle	une seule variable Theorem<Grid>
Accès cellule	g.Cells[i][j] (indexation C# naturelle)
Contrainte ligne	Z3Methods.Distinct(...) sur une ligne
Contrainte colonne	Z3Methods.Distinct(...) sur une colonne

Points clés : 1. Aucune manipulation de ArrayExpr, MkSelect, MkStore — le binding traduit g.Cells[i][j] en select(select(grid, i), j) automatiquement 2. La capture var (r, c) = (i, j) fige les indices de boucle dans la closure (piège classique des lambdas en boucle) 3. Z3Methods.Distinct est un marqueur LINQ : son corps lève NotSupportedException hors d’un théorème, mais le visiteur d’expressions le traduit en distinct SMT

2. Sudoku 4x4 — le cas d’usage canonique

Le Sudoku 4x4 ajoute aux contraintes du Latin Square une contrainte de blocs 2x2 : chaque bloc doit contenir des valeurs distinctes. C’est le cas d’usage canonique des grilles 2D, et l’API déclarative le rend particulièrement lisible.

Contrainte	Encodage lambda
Borne	g.Cells[i][j] >= 1 && <= 4
Ligne	Distinct(g.Cells[i][0..3])
Colonne	Distinct(g.Cells[0..3][j])
Bloc 2x2	Distinct des 4 cellules du bloc
Indice pré-rempli	g.Cells[i][j] == v

Nous plaçons quelques indices (pré-remplis) et laissons Z3 compléter la grille. La grille 4x4 (et non 9x9) est choisie pour rester instantanée — la résolution d’un Sudoku 9x9 complet via Theorem<Grid> est possible (cf. SudokuGridTheorem.cs) mais demande quelques centaines de millisecondes.

// Exemple 2 : Sudoku 4x4 via Theorem<Grid4> (lignes + colonnes + blocs 2x2)
int N = 4, B = 2;  // N = taille, B = cote de bloc (2 => blocs 2x2)

var ctx2 = new Z3Context();
var theorem2 = ctx2.NewTheorem<Grid4>();

// Bornes : 1 <= Cells[i][j] <= 4
for (int i = 0; i < N; i++)
    for (int j = 0; j < N; j++)
    {
        var (r, c) = (i, j);
        theorem2 = theorem2.Where(g => g.Cells[r][c] >= 1 && g.Cells[r][c] <= N);
    }

// Lignes distinctes
for (int i = 0; i < N; i++)
{
    var r = i;
    theorem2 = theorem2.Where(g => Z3Methods.Distinct(
        g.Cells[r][0], g.Cells[r][1], g.Cells[r][2], g.Cells[r][3]));
}

// Colonnes distinctes
for (int j = 0; j < N; j++)
{
    var c = j;
    theorem2 = theorem2.Where(g => Z3Methods.Distinct(
        g.Cells[0][c], g.Cells[1][c], g.Cells[2][c], g.Cells[3][c]));
}

// Blocs 2x2 distincts
for (int bi = 0; bi < B; bi++)
    for (int bj = 0; bj < B; bj++)
    {
        var (br, bc) = (bi, bj);
        theorem2 = theorem2.Where(g => Z3Methods.Distinct(
            g.Cells[br * B][bc * B],       g.Cells[br * B][bc * B + 1],
            g.Cells[br * B + 1][bc * B],   g.Cells[br * B + 1][bc * B + 1]));
    }

// Indices pre-remplis (0 = case vide)
// 1 _ | 3 _        1 4 | 3 2
// _ 2 | _ _   =>   3 2 | 1 4
// ----+----        ----+----
// _ _ | _ 1        2 3 | 4 1
// _ _ | 2 _        4 1 | 2 3
int[,] clues = new int[,] {
    { 1, 0, 3, 0 },
    { 0, 2, 0, 0 },
    { 0, 0, 0, 1 },
    { 0, 0, 2, 0 }
};
for (int i = 0; i < N; i++)
    for (int j = 0; j < N; j++)
        if (clues[i, j] != 0)
        {
            var (r, c, v) = (i, j, clues[i, j]);
            theorem2 = theorem2.Where(g => g.Cells[r][c] == v);
        }

var sw2 = Stopwatch.StartNew();
var solved = theorem2.Solve();
sw2.Stop();

DisplayGrid(solved.Cells, "Sudoku 4x4 (declaratif)", box: B);
Console.WriteLine($"Temps de resolution : {sw2.Elapsed.TotalMilliseconds:F1} ms");

=== Sudoku 4x4 (declaratif) (4x4) ===
  1 4 | 3 2
  3 2 | 1 4
  ---------
  2 3 | 4 1
  4 1 | 2 3
Temps de resolution : 40,8 ms

Interprétation 2 — Sudoku 4x4 déclaratif

Sortie obtenue : le Sudoku 4x4 est résolu avec lignes, colonnes et blocs 2x2 valides.

Contrainte	Clauses	Complexité
Bornes	N² = 16	O(N²)
Lignes	N × 6 = 24	O(N³)
Colonnes	N × 6 = 24	O(N³)
Blocs	4 × 6 = 24	O(N³)
Indices	6 égalités	—

Points clés : 1. La contrainte de bloc 2x2 se code en une seule lambda Distinct listant les 4 cellules du bloc — à comparer à la double-boucle nécessaire en API raw 2. Les indices pré-remplis sont de simples égalités g.Cells[i][j] == v, ajoutées par .Where() 3. Scalabilité : pour un Sudoku 9x9, Theorem<Grid> fonctionne (≈ 600 ms, cf. SudokuGridTheorem.cs) mais la construction des 729 contraintes lambda ralentit la phase de setup ; pour des grilles plus grandes, il vaut mieux se restreindre à des sous-ensembles ou utiliser l’API raw avec MkDistinct global

3. Carré magique — sommes de lignes et colonnes

Un autre usage des grilles 2D est la vérification de propriétés globales, comme la somme de chaque ligne et colonne. Un carré magique d’ordre N (N impair) est une grille NxN où chaque ligne, colonne et diagonale somme à la même valeur S = N(N²+1)/2. L’API déclarative exprime ces sommes par accumulation de Cells[i][j].

Note : Z3Methods.Distinct existe, mais il n’y a pas de sucre pour “somme” — on accumule les cellules dans une expression arithmétique a + b + c que le visiteur traduit en MkAdd.

// Exemple 3 : Carre magique 3x3 via Theorem<Grid3> (sommes lignes + colonnes = 15)
int N3 = 3;

var ctx3 = new Z3Context();
var theorem3 = ctx3.NewTheorem<Grid3>();

int S = N3 * (N3 * N3 + 1) / 2;   // 15 pour N=3
Console.WriteLine($"Somme magique pour N={N3} : S = {S}");

// Bornes : 1 <= Cells[i][j] <= N*N (=9)
for (int i = 0; i < N3; i++)
    for (int j = 0; j < N3; j++)
    {
        var (r, c) = (i, j);
        theorem3 = theorem3.Where(g => g.Cells[r][c] >= 1 && g.Cells[r][c] <= N3 * N3);
    }

// Tous distincts (necessaire pour un carre magique normal)
theorem3 = theorem3.Where(g => Z3Methods.Distinct(
    g.Cells[0][0], g.Cells[0][1], g.Cells[0][2],
    g.Cells[1][0], g.Cells[1][1], g.Cells[1][2],
    g.Cells[2][0], g.Cells[2][1], g.Cells[2][2]));

// Somme de chaque ligne = S
for (int i = 0; i < N3; i++)
{
    var r = i;
    theorem3 = theorem3.Where(g =>
        g.Cells[r][0] + g.Cells[r][1] + g.Cells[r][2] == S);
}

// Somme de chaque colonne = S
for (int j = 0; j < N3; j++)
{
    var c = j;
    theorem3 = theorem3.Where(g =>
        g.Cells[0][c] + g.Cells[1][c] + g.Cells[2][c] == S);
}

// Fixer le centre = 5 (propriété des carrés magiques 3x3 d'ordre impair)
theorem3 = theorem3.Where(g => g.Cells[1][1] == 5);

var sw3 = Stopwatch.StartNew();
var magic = theorem3.Solve();
sw3.Stop();

Console.WriteLine();
for (int i = 0; i < N3; i++)
    Console.WriteLine($"  [{string.Join(", ", magic.Cells[i])}]  somme = {magic.Cells[i].Sum()}");
Console.WriteLine($"Somme magique verifiee : S = {S}");
Console.WriteLine($"Temps de resolution : {sw3.Elapsed.TotalMilliseconds:F1} ms");

Somme magique pour N=3 : S = 15

  [2, 7, 6]  somme = 15
  [9, 5, 1]  somme = 15
  [4, 3, 8]  somme = 15
Somme magique verifiee : S = 15
Temps de resolution : 42,4 ms

Interprétation 3 — Carré magique déclaratif

Sortie obtenue : un carré magique 3x3 où toutes les lignes et colonnes somment à 15.

Aspect	Détail
Somme ligne	g.Cells[i][0] + g.Cells[i][1] + g.Cells[i][2] == S
Somme colonne	g.Cells[0][j] + g.Cells[1][j] + g.Cells[2][j] == S
Distincts	Z3Methods.Distinct sur les 9 cellules

Points clés : 1. L’accumulation arithmétique a + b + c est traduite par le visiteur en MkAdd sur les select imbriqués — aucun cast ArithExpr à gérer manuellement 2. Fixer le centre à 5 exploite la propriété mathématique des carrés magiques d’ordre impair (le médian occupe toujours le centre) 3. Comparé à l’API raw, la lisibilité est drastique : une contrainte de somme tient sur une ligne lisible

4. Comparaison — l’API raw Microsoft.Z3 (Store/Select imbriqués)

L’API déclarative Theorem<Grid> repose, en interne, sur l’API raw de Microsoft.Z3. Il est instructif de voir l’équivalent pour comprendre ce que le binding automatise. Voici le même Latin Square 3x3 (lignes distinctes) codé directement avec MkSelect imbriqués.

Un tableau imbriqué a le type SMT Array Int (Array Int Int). L’accès à la cellule (i, j) se fait par deux Select imbriqués :

\[ \text{grid}[i][j] = \text{select}(\text{select}(\text{grid},\; i),\; j) \]

Concept	SMT-LIB	C# (Microsoft.Z3)
Grille 2D	(Array Int (Array Int Int))	ctx.MkArrayConst("g", ctx.IntSort, ctx.MkArraySort(ctx.IntSort, ctx.IntSort))
Lire cellule	(select (select g i) j)	ctx.MkSelect((ArrayExpr)ctx.MkSelect(grid, i), j)
Écrire cellule	(store g i (store (select g i) j v))	ctx.MkStore(grid, i, ctx.MkStore(row, j, v))

// Comparaison : meme Latin Square 3x3 mais en API RAW Microsoft.Z3
// (lignes distinctes uniquement, pour la lisibilite de la comparaison)
using (var rctx = new Microsoft.Z3.Context())
{
    int N = 3;
    var rowSort = rctx.MkArraySort(rctx.IntSort, rctx.IntSort);
    var grid = rctx.MkArrayConst("grid", rctx.IntSort, rowSort);

    var solver = rctx.MkSolver();

    // Bornes + distincts par ligne : chaque MkSelect doit etre caste en ArrayExpr/ArithExpr
    for (int i = 0; i < N; i++)
    {
        var row = (ArrayExpr)rctx.MkSelect(grid, rctx.MkInt(i));
        for (int j = 0; j < N; j++)
        {
            var cell = (ArithExpr)rctx.MkSelect(row, rctx.MkInt(j));
            solver.Assert(rctx.MkGe(cell, rctx.MkInt(1)));
            solver.Assert(rctx.MkLe(cell, rctx.MkInt(N)));
        }
        for (int j1 = 0; j1 < N; j1++)
            for (int j2 = j1 + 1; j2 < N; j2++)
                solver.Assert(rctx.MkNot(rctx.MkEq(
                    rctx.MkSelect(row, rctx.MkInt(j1)),
                    rctx.MkSelect(row, rctx.MkInt(j2)))));
    }

    if (solver.Check() == Status.SATISFIABLE)
    {
        var model = solver.Model;
        Console.WriteLine("Latin Square 3x3 (API RAW, lignes distinctes) :");
        for (int i = 0; i < N; i++)
        {
            var row = (ArrayExpr)rctx.MkSelect(grid, rctx.MkInt(i));
            var cells = new List<int>();
            for (int j = 0; j < N; j++)
            {
                var cell = rctx.MkSelect(row, rctx.MkInt(j));
                cells.Add(int.Parse(model.Eval(cell).ToString()));
            }
            Console.WriteLine($"  Ligne {i}: [{string.Join(", ", cells)}]");
        }
    }
}

Latin Square 3x3 (API RAW, lignes distinctes) :
  Ligne 0: [1, 2, 3]
  Ligne 1: [1, 2, 3]
  Ligne 2: [1, 2, 3]

Interprétation 4 — Déclaratif vs Raw

Sortie obtenue : le même type de grille 3x3 (lignes distinctes), produit par deux API différentes.

Critère	Theorem<Grid> (déclaratif)	API raw Microsoft.Z3
Accès cellule	g.Cells[i][j]	MkSelect((ArrayExpr)MkSelect(grid, i), j)
Casts	aucun	(ArrayExpr), (ArithExpr) partout
Distinct	Z3Methods.Distinct(...)	boucle de MkNot(MkEq(...)) par paire
Modèle	solution.Cells[i][j] (int)	int.Parse(model.Eval(cell).ToString())
Niveau d’abstraction	haut (LINQ)	bas (SMT direct)

Quand utiliser quoi ? 1. Déclaratif (Theorem<Grid>) : prototypes pédagogiques, grilles jusqu’à 9x9, lisibilité prioritaire 2. Raw (Microsoft.Z3) : performances critiques, grilles très larges (optimisation par MkDistinct global), accès fin aux tactiques du solveur

5. Raw avancé — Store imbriqué (mise à jour d’une cellule)

La mise à jour d’une cellule (i, j) — opération d’écriture — n’a pas d’équivalent direct dans l’API déclarative (un théorème décrit une grille solution, il ne la modifie pas séquentiellement). C’est donc une opération strictement raw. Elle nécessite deux Store imbriqués (axiomes de McCarthy) :

\[ \text{grid}' = \text{store}(\text{grid},\; i,\; \text{store}(\text{select}(\text{grid},\; i),\; j,\; v)) \]

Cette section, conservée de l’édition précédente, montre le pattern fondamental des mises à jour de grilles (utile en vérification impérative : Sudoku incrémental, damier évolutif).

// Exemple raw : Store imbrique - mise a jour d'une cellule dans une grille 2D
using (var sctx = new Microsoft.Z3.Context())
{
    int N = 3;
    var rowSort = sctx.MkArraySort(sctx.IntSort, sctx.IntSort);
    var grid = sctx.MkArrayConst("g", sctx.IntSort, rowSort);

    // Initialiser [[1,2,3],[4,5,6],[7,8,9]] par Store imbriques
    ArrayExpr initGrid = grid;
    int[][] initData = new int[][] { new[]{1,2,3}, new[]{4,5,6}, new[]{7,8,9} };
    for (int i = 0; i < N; i++)
    {
        var row = (ArrayExpr)sctx.MkSelect(initGrid, sctx.MkInt(i));
        ArrayExpr newRow = row;
        for (int j = 0; j < N; j++)
            newRow = (ArrayExpr)sctx.MkStore(newRow, sctx.MkInt(j), sctx.MkInt(initData[i][j]));
        initGrid = (ArrayExpr)sctx.MkStore(initGrid, sctx.MkInt(i), newRow);
    }

    // Store imbrique : grid[1][2] = 99
    var row1 = (ArrayExpr)sctx.MkSelect(initGrid, sctx.MkInt(1));
    var updatedGrid = sctx.MkStore(initGrid, sctx.MkInt(1),
        sctx.MkStore(row1, sctx.MkInt(2), sctx.MkInt(99)));

    // Affichage des valeurs concretes : il faut un modele (Check SAT trivial,
    // aucune contrainte) pour que model.Eval replie les Store en valeurs.
    var dispSolver = sctx.MkSolver();
    dispSolver.Check();   // SAT : pas de contraintes => modele trivial
    var model = dispSolver.Model;
    Console.WriteLine("Apres store(grid, 1, store(row1, 2, 99)) :");
    for (int i = 0; i < N; i++)
    {
        var r = (ArrayExpr)sctx.MkSelect(updatedGrid, sctx.MkInt(i));
        var cells = new List<int>();
        for (int j = 0; j < N; j++)
        {
            var c = sctx.MkSelect(r, sctx.MkInt(j));
            cells.Add(int.Parse(model.Eval(c).ToString()));
        }
        Console.WriteLine($"  [{string.Join(", ", cells)}]");
    }

    // Verification formelle : grid'[1][2] == 99 (TOUJOURS VRAI si UNSAT sur la negation)
    var cell12 = sctx.MkSelect((ArrayExpr)sctx.MkSelect(updatedGrid, sctx.MkInt(1)), sctx.MkInt(2));
    var chk = sctx.MkSolver();
    chk.Assert(sctx.MkNot(sctx.MkEq(cell12, sctx.MkInt(99))));
    Console.WriteLine($"grid'[1][2] == 99 : {(chk.Check() == Status.UNSATISFIABLE ? "TOUJOURS VRAI" : "PEUT ETRE FAUX")}");
    Console.WriteLine("Store imbrique verifie : seule la cellule (1,2) a change.");
}

Apres store(grid, 1, store(row1, 2, 99)) :
  [1, 2, 3]
  [4, 5, 99]
  [7, 8, 9]
grid'[1][2] == 99 : TOUJOURS VRAI
Store imbrique verifie : seule la cellule (1,2) a change.

Interprétation 5 — Store imbriqué

Sortie obtenue : [[1,2,3], [4,5,6], [7,8,9]] devient [[1,2,3], [4,5,99], [7,8,9]].

Étape	Opération	Effet
1	row = select(grid, 1)	extraire la ligne 1
2	row' = store(row, 2, 99)	mettre à jour la cellule (1,2)
3	grid' = store(grid, 1, row')	réinsérer la ligne modifiée

Points clés : 1. Le store imbriqué préserve la localité : seule la cellule ciblée est modifiée (axiome read-over-write de McCarthy) 2. C’est le pattern fondamental pour les mises à jour impératives de grilles, hors paradigme déclaratif 3. L’absence d’équivalent déclaratif est fondée : un théorème est une spécification relationnelle, pas un programme séquentiel

6. Exercices

Les exercices suivants utilisent l’API déclarative Theorem<Grid>. Chaque stub se contente d’un print/Console.WriteLine de confirmation (convention C.1 : aucune erreur volontaire) — à vous de remplir la solution.

Exercice 1 : Latin Square avec contraintes diagonales

Objectif : ajoutez les contraintes de diagonales au Latin Square 3x3 de l’exemple 1. Un Latin Square diagonal exige que chaque diagonale contienne également des valeurs distinctes.

Indices : - Diagonale principale : g.Cells[0][0], g.Cells[1][1], g.Cells[2][2] doivent être distincts - Diagonale anti-principale : g.Cells[0][2], g.Cells[1][1], g.Cells[2][0] doivent être distincts - Reprenez le code de l’exemple 1 (bornes + lignes + colonnes) et ajoutez les deux Z3Methods.Distinct de diagonales - Fixez la première ligne à [1, 2, 3] pour réduire la symétrie

// Exercice 1 : Latin Square 3x3 avec contraintes diagonales (API declarative)
// TODO etudiant : ajoutez les contraintes de diagonales au Latin Square
// Etape 1 : reprenez le code de l'exemple 1 (bornes + lignes + colonnes distinctes)
// Etape 2 : ajoutez Distinct(g.Cells[0][0], g.Cells[1][1], g.Cells[2][2])
// Etape 3 : ajoutez Distinct(g.Cells[0][2], g.Cells[1][1], g.Cells[2][0])
// Indice : chaque contrainte est un theorem.Where(g => Z3Methods.Distinct(...))

Console.WriteLine("Exercice a completer : Latin Square 3x3 avec diagonales distinctes");

Exercice a completer : Latin Square 3x3 avec diagonales distinctes

Exercice 2 : Sudoku 4x4 avec grille de départ différente

Objectif : résolvez le Sudoku 4x4 avec un autre jeu d’indices, puis vérifiez que la solution satisfait toutes les contraintes (lignes, colonnes, blocs).

Indices : - Reprenez la construction du théorème de l’exemple 2 (bornes + lignes + colonnes + blocs) - Utilisez les indices suivants (0 = vide) : _ 3 | _ _ _ _ | _ 2 ----+---- 4 _ | _ _ _ _ | 1 _ - Ajoutez chaque indice par theorem.Where(g => g.Cells[i][j] == v) - Affichez la solution avec DisplayGrid

// Exercice 2 : Sudoku 4x4 avec une autre grille de depart (API declarative)
// TODO etudiant : construisez le theoreme et ajoutez les indices ci-dessus
// Etape 1 : reprenez bornes + lignes + colonnes + blocs 2x2 de l'exemple 2
// Etape 2 : ajoutez les 4 indices (Cells[0][1]==3, Cells[1][3]==2, Cells[2][0]==4, Cells[3][2]==1)
// Etape 3 : resolvez et affichez avec DisplayGrid(..., box: 2)
// Indice : tous les indices aboutissent a une solution unique

Console.WriteLine("Exercice a completer : Sudoku 4x4 avec autre grille de depart");

Exercice a completer : Sudoku 4x4 avec autre grille de depart

Exercice 3 : Vérificateur de carré magique (approche déclarative)

Objectif : vérifiez si la grille suivante est un carré magique (lignes, colonnes ET les deux diagonales somment à 15) en modélisant le problème inverse : contraindre la grille à valoir ces nombres, puis vérifier que les contraintes de somme sont satisfaites.

[2, 7, 6]
[9, 5, 1]
[4, 3, 8]

Indices : - Construisez un Theorem<Grid> et fixez chaque cellule à sa valeur (g.Cells[i][j] == v) - Ajoutez les contraintes “somme ligne = 15”, “somme colonne = 15”, “somme diagonale = 15” - Si Solve() retourne une solution, la grille satisfait toutes les contraintes → c’est un carré magique - Variante : retirez la contrainte de diagonale et observez si le verdict change

// Exercice 3 : Verificateur de carre magique declaratif
// TODO etudiant : verifiez si [[2,7,6],[9,5,1],[4,3,8]] est un carre magique
// Etape 1 : fixez chaque cellule a sa valeur (9 contraintes d'egalite)
// Etape 2 : ajoutez sommes de lignes = 15, colonnes = 15, 2 diagonales = 15
// Etape 3 : si Solve() reussit, la grille est un carre magique valide
// Indice : c'est bien un carre magique, toutes les contraintes doivent etre satisfiables

Console.WriteLine("Exercice a completer : verificateur de carre magique");

Exercice a completer : verificateur de carre magique

Conclusion

Ce notebook a montré comment modéliser des grilles 2D via l’API déclarative Theorem<Grid> du binding LINQ Z3.Linq (support int[][]), en contraste avec l’API raw Microsoft.Z3.

Récapitulatif : déclaratif vs raw

Concept	Déclaratif Theorem<Grid>	Raw Microsoft.Z3
Grille 2D	propriété int[][] Cells	MkArraySort(IntSort, MkArraySort(IntSort, IntSort))
Accès cellule	g.Cells[i][j]	MkSelect((ArrayExpr)MkSelect(grid, i), j)
Distinct	Z3Methods.Distinct(...)	boucle de MkNot(MkEq(...))
Mise à jour (Store)	(non applicable)	MkStore(grid, i, MkStore(row, j, v))
Niveau d’abstraction	LINQ / haut	SMT / bas

Points clés à retenir

1. Theorem<Grid> + Cells[i][j] = grille 2D lisible, contraintes en lambdas naturelles
2. Capture de closure : var (r, c) = (i, j) fige les indices de boucle (piège classique)
3. Z3Methods.Distinct = sucre LINQ traduit en distinct SMT par le visiteur d’expressions
4. Raw pour les mises à jour : le Store imbriqué est strictement impératif (pas d’équivalent déclaratif)
5. Scalabilité : l’API déclarative excelle jusqu’à 9x9 ; au-delà, préférer l’API raw avec MkDistinct global ou restreindre à des sous-ensembles

Résolution du package (rappel technique)

Le support int[][] de Theorem<T> n’est pas encore publié sur NuGet (le paquet public Z3.Linq 2.0.1 ne gère qu’un niveau de collection). Ce notebook charge donc le fork local (commit 096a638, branche #1206) via des DLL compilées. Pour (re)générer le dossier .deploy/, lancez le script dédié (une fois par machine) :

# Windows
scripts/environment/z3-build-deploy.ps1
# Linux / macOS
scripts/environment/z3-build-deploy.sh

Ce script ne recompile pas Z3 : il construit uniquement le wrapper fin Z3.Linq.csproj (~1.5 s), puis copie le solveur natif Microsoft.Z3 et MiaPlaza.ExpressionUtils depuis le cache NuGet public à côté de Z3.Linq.dll dans .deploy/. Décision ai-01 [DECISION COORD] 2026-06-13, option (b).

Lorsque le fork sera publié sur NuGet (version ≥ 2.0.2 avec int[][]), ce notebook pourra revenir au #r "nuget: Z3.Linq" standard utilisé par les notebooks 01-04.

---

Navigation : Index SymbolicAI | Série Z3 | << Array Theory | Meal Planner >>