Sudoku 4x4 : comparaison des modes `Array` et `Constants`

Navigation : Index SymbolicAI | Série Z3 | << Sudoku Theorem vs Array | Array Theory >>

Objectif

Ce notebook démontre les deux modes de modélisation des collections offerts par le fork Z3.Linq, en résolvant le même Sudoku 4x4 (int[][]) des deux façons. C’est la démonstration directe que l’enum CollectionHandling — historiquement du dead code défini mais jamais câblé — est désormais vivante et fonctionnelle bout-en-bout.

Mode	Modélisation Z3	Avantage
`Array` (défaut)	Une seule `ArrayExpr` Z3 + `Select`/`Store` (théorie des tableaux)	Compact, supporte les index symboliques, `int[][]` imbriqué
`Constants`	Un constant Z3 par élément (`Cells_0_0`, `Cells_0_1`, …)	Modèle « un symbole = une inconnue », proche du raisonnement humain, lisible dans le solver

Les deux modes produisent une solution valide ; le choix est pédagogique et dépend de ce qu’on veut illustrer.

Vue d’ensemble : un même Sudoku, deux modes d’encodage des collections

flowchart TB
    G["Même grille Sudoku 4x4\n(int de int)"]
    G --> M1["Mode Array (defaut)"]
    G --> M2["Mode Constants"]
    M1 --> A1["1 seule ArrayExpr Z3\n+ Select / Store\n(théorie des tableaux)"]
    M2 --> C1["1 constant Z3 par cellule\nCells_0_0, Cells_0_1, ..."]
    A1 --> S["Solution valide\n(carre latin)"]
    C1 --> S
    S --> CH["CollectionHandling\ndesormais cable bout-en-bout\n(dead code ressuscite)"]
    %% 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 M1 fill:#c8f7c5,color:#1b5e20
    style A1 fill:#c8f7c5,color:#1b5e20
    style M2 fill:#cfe3ff,color:#004085
    style C1 fill:#cfe3ff,color:#004085

Les deux modes resolvent le même int[][] et convergent vers une solution valide. Le mode Array (vert) encode la grille avec une seule ArrayExpr ; le mode Constants (bleu) créé un symbole Z3 par cellule. C’est la demonstration directe que l’enum CollectionHandling est desormais vivante et fonctionnelle.

Configuration de l’environnement

Chargement du fork Z3.Linq (avec CollectionHandling câblé) depuis le sous-module local. Les DLL sont produites par le script scripts/environment/z3-build-deploy.ps1 (décision ai-01 2026-06-13, option b).

Le jumeau Linux/macOS scripts/environment/z3-build-deploy.sh produit les mêmes DLL avec les mêmes commandes dotnet (cf. la cellule pré-requis de 05_Nested_Arrays_2D, qui nomme les deux chemins).

#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.Linq;

Console.WriteLine($"Z3.Linq chargé. CollectionHandling disponible : {nameof(CollectionHandling.Array)}, {nameof(CollectionHandling.Constants)}");

Z3.Linq chargé. CollectionHandling disponible : Array, Constants

Type de grille et théorème Sudoku 4x4

On définit une grille 4x4 comme un int[][]. Le théorème impose : chaque cellule dans [1,4], chaque ligne et chaque colonne a 4 valeurs distinctes (carré latin).

public class SudokuGrid4
{
    public int[][] Cells { get; set; } = new int[4][];
    public SudokuGrid4()
    {
        for (int i = 0; i < 4; i++) Cells[i] = new int[4];
    }
}

// Construit le théorème Sudoku 4x4 (sans contraintes d'indices) sur un Z3Context donné.
// Le mode de collection est hérité du contexte (Array ou Constants).
public static Theorem<SudokuGrid4> BuildSudoku(Z3Context ctx)
{
    var t = ctx.NewTheorem<SudokuGrid4>();
    for (int i = 0; i < 4; i++)
        for (int j = 0; j < 4; j++)
        {
            int i1 = i, j1 = j;
            t = t.Where(g => g.Cells[i1][j1] >= 1 && g.Cells[i1][j1] <= 4);
        }
    for (int r = 0; r < 4; r++)
    {
        int r1 = r;
        t = t.Where(g => Z3Methods.Distinct(g.Cells[r1][0], g.Cells[r1][1], g.Cells[r1][2], g.Cells[r1][3]));
    }
    for (int c = 0; c < 4; c++)
    {
        int c1 = c;
        t = t.Where(g => Z3Methods.Distinct(g.Cells[0][c1], g.Cells[1][c1], g.Cells[2][c1], g.Cells[3][c1]));
    }
    return t;
}

public static string GridToString(SudokuGrid4 g) =>
    string.Join("\n", Enumerable.Range(0, 4).Select(r => string.Join(" ", g.Cells[r])));

Résolution en mode `Array` (théorie des tableaux Z3)

C’est le mode par défaut. Cells est modélisé comme une seule ArrayExpr Z3 (avec une dimension imbriquée pour int[][]). L’accès Cells[i][j] se traduit par Select(Select(arr, i), j).

var ctxArray = new Z3Context { DefaultCollectionHandling = CollectionHandling.Array };
Console.WriteLine($"Mode actif : {ctxArray.DefaultCollectionHandling}");

var solArray = BuildSudoku(ctxArray).Solve();
Console.WriteLine("Solution (mode Array) :");
Console.WriteLine(GridToString(solArray));

Mode actif : Array
Solution (mode Array) :
2 3 4 1
3 4 1 2
4 1 2 3
1 2 3 4

Résolution en mode `Constants` (un constant Z3 par cellule)

Ici, Cells est représenté par un constant Z3 par élément : Cells_0_0, Cells_0_1, …, Cells_3_3 (16 symboles). C’est le modèle classique de la librairie historique, ressuscité dans le fork. L’accès Cells[i][j] crée paresseusement le constant Cells_i_j lors de sa première utilisation.

Le même code BuildSudoku est réutilisé — seule la configuration du Z3Context change. C’est la preuve que les deux modes coexistent proprement.

var ctxConst = new Z3Context { DefaultCollectionHandling = CollectionHandling.Constants };
Console.WriteLine($"Mode actif : {ctxConst.DefaultCollectionHandling}");

var solConst = BuildSudoku(ctxConst).Solve();
Console.WriteLine("Solution (mode Constants) :");
Console.WriteLine(GridToString(solConst));

Mode actif : Constants
Solution (mode Constants) :
2 3 4 1
3 4 1 2
4 1 2 3
1 2 3 4

Vérification : les deux solutions sont des carrés latins valides

Indépendamment du mode, le résultat doit satisfaire les contraintes (lignes et colonnes = permutations de 1..4).

bool IsLatinSquare(SudokuGrid4 g)
{
    var expected = new int[] { 1, 2, 3, 4 };
    for (int r = 0; r < 4; r++)
        if (!g.Cells[r].OrderBy(v => v).SequenceEqual(expected)) return false;
    for (int c = 0; c < 4; c++)
    {
        var col = Enumerable.Range(0, 4).Select(r => g.Cells[r][c]).OrderBy(v => v);
        if (!col.SequenceEqual(expected)) return false;
    }
    return true;
}

Console.WriteLine($"Array     valide ? {IsLatinSquare(solArray)}");
Console.WriteLine($"Constants valide ? {IsLatinSquare(solConst)}");

Array     valide ? True
Constants valide ? True

Interprétation : pourquoi les deux modes convergent-ils vers la même solution ?

Vous aurez remarqué un fait frappant : les deux modes produisent exactement la même grille :

Ce n’est pas une coïncidence, et ce n’est pas non plus un défaut. C’est précisément ce que doit garantir une abstraction bien conçue :

Question	Réponse
Pourquoi la même solution ?	Les deux modes résolvent le même théorème (mêmes contraintes LINQ), Z3 explore donc le même espace de solutions et converge vers la même solution minimale.
Le mode change-t-il la sémantique ?	Non. `CollectionHandling` est un paramètre d’encodage, pas de signification. Le CSP (carré latin 4x4) est invariant.
Que change le mode alors ?	La représentation interne envoyée au solver : une `ArrayExpr` (mode Array) vs 16 constantes nommées (mode Constants).

Leçon clé : c’est la preuve que le mode Constants est bien vivant. Si l’enum était encore du dead code non câblé (son état historique), le mode Constants aurait soit échoué silencieusement, soit reproduit le comportement Array par défaut. Ici, il résout réellement le CSP via des symboles séparés — le chemin d’exécution est distinct, le résultat est identique par correction.

Indice pédagogique — quand utiliser quel mode ?

Array : quand on veut un modèle compact ou qu’on manipule des index symboliques (ex. « existe-t-il un index k tel que… »). C’est aussi le seul mode qui supporte nativement le int[][] imbriqué via la théorie des tableaux.
Constants : quand on veut qu’apparaissent dans le solver des symboles nommés explicites (Cells_2_3 = 4), par exemple pour inspecter le modèle, pour enseigner la notion d’inconnue, ou quand la taille de la collection est fixe et petite.

Les deux se valent en puissance d’expression pour les CSP statiques comme le Sudoku ; c’est une question de lisibilité et de stratégie de résolution.

Exercices

Exercice 1 — Hint dans les deux modes

Ajoutez la contrainte g.Cells[0][0] == 2 au théorème et vérifiez que la solution la respecte dans les deux modes. Affichez les deux grilles.

// Exercice 1 à compléter
// Indice : reprenez BuildSudoku, ajoutez .Where(g => g.Cells[0][0] == 2), solvez dans les deux contextes.
Console.WriteLine("Exercice à compléter");

Exercice à compléter

Exercice 2 — Sudoku 9x9 en mode `Constants`

Définissez un SudokuGrid9 (9x9) et un théorème avec contraintes de lignes, colonnes et blocs 3x3. Résolvez-le en mode Constants. Indice : un bloc partant en (br, bc) contient les cellules Cells[br*3 + di][bc*3 + dj] pour di, dj ∈ {0,1,2}.

// Exercice 2 à compléter
Console.WriteLine("Exercice à compléter");

Exercice à compléter

Exercice 3 — Comparaison empirique des deux modes

Mesurez le temps de résolution d’un Sudoku 9x9 (avec quelques indices fixés) en mode Array puis en mode Constants avec System.Diagnostics.Stopwatch. Que constatez-vous ? Quelle hypothèse pouvez-vous formuler sur l’impact du nombre de symboles Z3 sur le temps de résolution ?

// Exercice 3 à compléter
// Indice : var sw = System.Diagnostics.Stopwatch.StartNew(); ... sw.Stop(); sw.ElapsedMilliseconds;
Console.WriteLine("Exercice à compléter");

Exercice à compléter

Conclusion

Ce notebook a démontré que l’enum CollectionHandling — historiquement du dead code défini mais jamais câblé dans le fork — est désormais fonctionnelle bout-en-bout.

Récapitulatif

Concept	Rôle dans la démonstration
`CollectionHandling.Array` (défaut)	Le mode existant : `int[][]` modélisé comme une `ArrayExpr` Z3 + `Select`/`Store`. Anti-régression (préserve le travail hand-typed).
`CollectionHandling.Constants`	Le mode ressuscité : un constant Z3 par élément (`Cells_i_j`). Était du dead code, maintenant câblé.
Même théorème, 2 encodages	`BuildSudoku` est réutilisé tel quel ; seul `Z3Context.DefaultCollectionHandling` change. Preuve de l’orthogonalité mode/sémantique.
Convergence des solutions	Les 2 modes produisent le même carré latin valide = correction de l’implémentation Constants.

Points clés à retenir

L’encodage n’est pas la sémantique : CollectionHandling change comment Z3 voit les collections, pas ce que le théorème exprime.
Le mode Constants expose des symboles nommés (Cells_2_3 = 4) — utile pour inspecter le modèle ou enseigner la notion d’inconnue.
Le mode Array est plus compact et supporte nativement les index symboliques et le int[][] imbriqué (voir Nested Arrays 2D).

Pour aller plus loin

Le notebook 06 — Meal Planner Hierarchical applique la même comparaison des deux modes à un cas réel (planification de repas avec coûts).
Les exercices ci-dessus vous font manipuler les deux modes sur des instances plus grandes (9x9) et mesurer leur impact sur les performances.