Sudoku 12b : Linq2Z3 — l’histoire d’un binding, de 81 propriétés aux tableaux imbriqués

<< Sudoku-12 Z3 C# | Index | Sudoku-13 Automates symboliques >>

Série : Sudoku (accrétion du notebook 12) · Kernel : .NET (C#) · Prérequis : Sudoku-12-Z3-CSharp (Z3 brut)

Vue d’ensemble : le même moteur, une couche d’expression fluente

Sudoku-12 résout le Sudoku avec l’API Z3 brute : on fabrique soi-même les IntExpr, les BoolExpr, on appelle solver.Check() puis on relit le modèle cellule par cellule. C’est la voie directe — et la plus verbeuse.

Il existe une autre voie : Linq2Z3 (bibliothèque Z3.Linq), un binding qui enveloppe le même moteur Z3 dans un DSL LINQ déclaratif. On décrit une classe C# ordinaire dont les propriétés sont les inconnues, puis on écrit les contraintes comme des prédicats .Where(...) :

var theorem = ctx.NewTheorem<SudokuGrid>();
theorem = theorem.Where(g => g.Cells[row][col] >= 1 && g.Cells[row][col] <= 9);
var solution = theorem.Solve();   // solution est une SudokuGrid remplie

Ce binding a une histoire : né en 2009 dans une série de trois articles de Bart De Smet, porté par nos soins dans le fork MyIntelligenceAgency/Z3.Linq, il a évolué en quatre rungs — quatre marches d’une échelle dont chaque barreau est porté par un artefact ou un commit tracé. Le Sudoku est l’application canonique de cette évolution : chaque rung se mesure sur lui.

Pourquoi une accrétion de Sudoku-12 et pas un nouveau numéro ? Le Linq2Z3 approfondit le palier Z3 (même solveur, couche d’expression plus riche) au lieu de l’étendre en un survol de plus — c’est la convention d’accrétion de la série (la base compte comme a, la première accrétion est b, réf. #5081).

Positionnement vis-à-vis de la série SMT. La série SymbolicAI/SMT/Z3-Linq2Z3/ enseigne le binding en profondeur (modélisation, modes, cas d’usage). Ce notebook est le pont côté série Sudoku : il raconte l’évolution du binding telle qu’elle se lit dans son code, ancrée à chaque marche. Pour la pratique de modélisation, voir 02 — Théorème vs Arrays et 05 — Tableaux imbriqués.

L’échelle des quatre barreaux

Barreau	Forme du modèle	Ancrage tracé	Ce qu’il apporte
1	une propriété int par cellule (81 pour un 9x9)	SudokuTable.cs, série d’articles 2009	le DSL existe : NewTheorem<T> / Where / Z3Methods.Distinct
2	collections indicées (List<int>, mode Constants)	branche feature/list-collection-constants-mode (notre port)	boucles et closures remplacent la réflexion
3	tableaux imbriqués int[][]	commit 096a638 — SudokuGrid.cs / SudokuGridTheorem.cs	le modèle ressemble enfin à la grille
4	tableaux rectangulaires int[,]	l’intention, confrontée au code réel	le rung manquant — attesté tel quel en section 4

Chaque barreau est démontré exécuté dans ce notebook, sur le même moteur Z3 que Sudoku-12.

Configuration de l’environnement

Le binding vit dans le sous-module SymbolicAI/SMT/Z3.Linq (fork de endjin/Z3.Linq), qui embarque un dossier .deploy/ préassemblé : les DLL Microsoft.Z3 (le moteur), Z3.Linq (le binding) et ExpressionUtils (dépendance de réécriture d’expressions).

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

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

Console.WriteLine($"Z3.Linq   v{typeof(Z3Context).Assembly.GetName().Version}");
Console.WriteLine($"Microsoft.Z3 v{typeof(Context).Assembly.GetName().Version}");
Console.WriteLine("Imports OK");

The below script needs to be able to find the current output cell; this is an easy method to get it.

Z3.Linq   v1.0.0.0
Microsoft.Z3 v4.12.2.0
Imports OK

Outils d’affichage

Une grille 1D aplatie (81 cellules, index i * 9 + j) et une grille imbriquée int[][] — les deux formes que les barreaux vont croiser.

void DisplayFlat(int[] cells, string title)
{
    Console.WriteLine($"--- {title} ---");
    var sep = new string('-', 25);
    Console.WriteLine(sep);
    for (int i = 0; i < 9; i++)
    {
        var sb = new StringBuilder("| ");
        for (int j = 0; j < 9; j++)
        {
            sb.Append(cells[i * 9 + j]);
            sb.Append((j + 1) % 3 == 0 ? " | " : " ");
        }
        Console.WriteLine(sb);
        if ((i + 1) % 3 == 0) Console.WriteLine(sep);
    }
}

void DisplayNested(int[][] cells, string title)
{
    Console.WriteLine($"--- {title} ---");
    var sep = new string('-', 25);
    Console.WriteLine(sep);
    for (int i = 0; i < 9; i++)
    {
        var sb = new StringBuilder("| ");
        for (int j = 0; j < 9; j++)
        {
            sb.Append(cells[i][j]);
            sb.Append((j + 1) % 3 == 0 ? " | " : " ");
        }
        Console.WriteLine(sb);
        if ((i + 1) % 3 == 0) Console.WriteLine(sep);
    }
}

// Le puzzle témoin de Wikipedia, utilisé par tous les barreaux.
int[] WIKI_PUZZLE = {
    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,
};

Console.WriteLine($"Puzzle temoin charge : {WIKI_PUZZLE.Count(v => v != 0)} indices non nuls");

Puzzle temoin charge : 30 indices non nuls

1. Barreau 1 — 2009 : le binding et son premier Sudoku, une propriété par cellule

L’origine est une série de trois articles de Bart De Smet (avril et septembre 2009, conservés sur archive.org et re-déposés dans le fork sous docs/blogs/) :

1. Exploring the Z3 Theorem Prover — le moteur ;
2. LINQ to the Unexpected — l’idée du binding : un « esoteric LINQ binding » où Where ne filtre pas une collection mais contraint un théorème ;
3. Theorem Solving on Steroids — le type Theorem<T> et le pattern de requête.

Le Sudoku d’origine du binding est SudokuTable.cs : une classe où chaque cellule est une propriété typée distincte — Cell11, Cell12, … Cell99, soit 81 propriétés int. Le théorème se construit avec une contrainte .Where(...) par propriété, et Z3Methods.Distinct(...) porte l’unicité.

Pour toucher ce rung du doigt sans recopier 220 lignes, voici sa déclinaison fidèle sur un Sudoku 4x4 (16 propriétés, valeurs 1 à 4, blocs 2x2) :

// Barreau 1 : la classe-modele, une propriete par cellule (forme de SudokuTable.cs)
public class SudokuTable4
{
    public int Cell11 { get; private set; }
    public int Cell12 { get; private set; }
    public int Cell13 { get; private set; }
    public int Cell14 { get; private set; }
    public int Cell21 { get; private set; }
    public int Cell22 { get; private set; }
    public int Cell23 { get; private set; }
    public int Cell24 { get; private set; }
    public int Cell31 { get; private set; }
    public int Cell32 { get; private set; }
    public int Cell33 { get; private set; }
    public int Cell34 { get; private set; }
    public int Cell41 { get; private set; }
    public int Cell42 { get; private set; }
    public int Cell43 { get; private set; }
    public int Cell44 { get; private set; }

    public override string ToString()
    {
        var names = new[] { "Cell11","Cell12","Cell13","Cell14","Cell21","Cell22","Cell23","Cell24",
                            "Cell31","Cell32","Cell33","Cell34","Cell41","Cell42","Cell43","Cell44" };
        var props = GetType().GetProperties();
        var sb = new StringBuilder();
        for (int i = 0; i < 4; i++)
        {
            for (int j = 0; j < 4; j++)
                sb.Append(props.Single(p => p.Name == names[i * 4 + j]).GetValue(this)).Append(' ');
            sb.AppendLine();
        }
        return sb.ToString();
    }
}

// L'astuce de SudokuTheorem.cs : les bornes 1..4 sont construites par reflexion,
// par nom de propriete — parce qu'une lambda ne peut PAS indexer t.Cell{i}{j}.
Expression<Func<SudokuTable4, bool>> Between1And4(string cellName)
{
    var t = Expression.Parameter(typeof(SudokuTable4), "t");
    var cell = Expression.Property(t, cellName);
    var one = Expression.Constant(1);
    var four = Expression.Constant(4);
    return Expression.Lambda<Func<SudokuTable4, bool>>(
        Expression.AndAlso(
            Expression.GreaterThanOrEqual(cell, one),
            Expression.LessThanOrEqual(cell, four)), t);
}

Console.WriteLine("SudokuTable4 : 16 proprietes, un nom par cellule — la forme du rung 1");

SudokuTable4 : 16 proprietes, un nom par cellule — la forme du rung 1

// Barreau 1 : le theoreme en 4x4 — domaines par reflexion, unites explicites, indices poses
var sw1 = Stopwatch.StartNew();
var ctx1 = new Z3Context();
var th1 = ctx1.NewTheorem<SudokuTable4>();

// (a) Domaines 1..4 : une contrainte par propriete, construite par reflexion
foreach (var name in new[] { "Cell11","Cell12","Cell13","Cell14","Cell21","Cell22","Cell23","Cell24",
                             "Cell31","Cell32","Cell33","Cell34","Cell41","Cell42","Cell43","Cell44" })
{
    th1 = th1.Where(Between1And4(name));
}

// (b) Unites : rangees, colonnes, blocs 2x2 — ecritures explicites, aucune boucle possible
th1 = th1.Where(t => Z3Methods.Distinct(t.Cell11, t.Cell12, t.Cell13, t.Cell14));
th1 = th1.Where(t => Z3Methods.Distinct(t.Cell21, t.Cell22, t.Cell23, t.Cell24));
th1 = th1.Where(t => Z3Methods.Distinct(t.Cell31, t.Cell32, t.Cell33, t.Cell34));
th1 = th1.Where(t => Z3Methods.Distinct(t.Cell41, t.Cell42, t.Cell43, t.Cell44));
th1 = th1.Where(t => Z3Methods.Distinct(t.Cell11, t.Cell21, t.Cell31, t.Cell41));
th1 = th1.Where(t => Z3Methods.Distinct(t.Cell12, t.Cell22, t.Cell32, t.Cell42));
th1 = th1.Where(t => Z3Methods.Distinct(t.Cell13, t.Cell23, t.Cell33, t.Cell43));
th1 = th1.Where(t => Z3Methods.Distinct(t.Cell14, t.Cell24, t.Cell34, t.Cell44));
th1 = th1.Where(t => Z3Methods.Distinct(t.Cell11, t.Cell12, t.Cell21, t.Cell22));
th1 = th1.Where(t => Z3Methods.Distinct(t.Cell13, t.Cell14, t.Cell23, t.Cell24));
th1 = th1.Where(t => Z3Methods.Distinct(t.Cell31, t.Cell32, t.Cell41, t.Cell42));
th1 = th1.Where(t => Z3Methods.Distinct(t.Cell33, t.Cell34, t.Cell43, t.Cell44));

// (c) Indices du puzzle 4x4 : les coins
th1 = th1.Where(t => t.Cell11 == 1);
th1 = th1.Where(t => t.Cell14 == 4);
th1 = th1.Where(t => t.Cell41 == 2);
th1 = th1.Where(t => t.Cell44 == 3);

var sol1 = th1.Solve();
sw1.Stop();

Console.WriteLine($"Resolution 4x4 en {sw1.ElapsedMilliseconds} ms");
Console.WriteLine();
Console.Write(sol1.ToString());

Resolution 4x4 en 145 ms

1 3 2 4 
4 2 3 1 
3 4 1 2 
2 1 4 3 

Interprétation 1 — le rung propriétés : le DSL existe, l’échelle n’existe pas encore

Le binding fonctionne dès 2009 : NewTheorem<SudokuTable4>() fabrique les 16 inconnues Z3 à partir des propriétés, chaque Where compile une expression C# en contrainte SMT, et Solve() rend une instance remplie de la classe — pas un modèle à relire index par index. C’est déjà un saut ergonomique énorme sur le Z3 brut de Sudoku-12.

Mais regardez ce que le code a dû faire pour tenir sur ce rung :

• la classe SudokuTable réelle compte 81 propriétés et 220 lignes (l’artefact la génère telle quelle) ;
• les bornes 1..9 de l’artefact sont construites par réflexion sur des noms en chaîne ("Cell{0}{1}", cf. SudokuTheorem.cs) — parce qu’une expression lambda ne peut pas écrire t.Cell{i}{j} ;
• les neuf contraintes Distinct de blocs du 9x9 sont écrites une à une, chacune avec neuf arguments nommés.

Sur notre 4x4, douze contraintes d’unité explicites ont suffi. Sur un 9x9 il en faut 27 ; sur un 16x16, 48 — et la classe doit d’abord exister, propriété par propriété. Le rung propriétés ne passe pas à l’échelle : c’est exactement le problème que le rung suivant vient résoudre.

2. Barreau 2 — notre port : les collections indicées (mode Constants)

Le deuxième rung est notre port du binding, porté par la branche feature/list-collection-constants-mode du fork : le théorème accepte désormais une collection indicée comme inconnue — List<int>, IList<int>, int[] — et le DSL gagne un réglage :

var ctx = new Z3Context { DefaultCollectionHandling = CollectionHandling.Constants };

Deux modes existent (enum CollectionHandling dans Environment.cs) :

• Array (le défaut) : la collection devient un tableau SMT (Store/Select) — l’unicité de l’objet est native côté Z3 ;
• Constants : la collection est éclatée en constantes individuelles, une par élément — le solveur voit 81 inconnues plates.

Le point technique qui explique la marche : un indexeur List<int> compile vers un appel de méthode get_Item, pas vers un nœud ArrayIndex comme int[] — le visitor du binding a dû apprendre à router les deux front-ends (c’est documenté dans ListCollectionTests.cs du fork, qui épingle les deux modes ensemble).

Le modèle 9x9 complet devient une classe de quatre lignes :

// Barreau 2 : le modele 9x9 complet en une propriete collection
public class SudokuArray
{
    public List<int> Cells { get; set; } = Enumerable.Repeat(0, 81).ToList();
}

// Le theoreme en mode Constants : boucles + closures, plus de reflexion
Theorem<SudokuArray> BuildArrayTheorem(Z3Context ctx)
{
    var th = ctx.NewTheorem<SudokuArray>();
    var idx = Enumerable.Range(0, 9).ToArray();

    // Domaines 1..9 : la boucle que le rung 1 ne pouvait pas ecrire
    for (int i = 0; i < 9; i++)
        for (int j = 0; j < 9; j++)
        {
            var i1 = i; var j1 = j;   // capture de closure : copie locale obligatoire
            th = th.Where(s => s.Cells[i1 * 9 + j1] > 0 && s.Cells[i1 * 9 + j1] < 10);
        }

    // Unites : rangees, colonnes, blocs — args explicites, la forme que le
    // rewriter Distinct epingle pour les deux modes (CollectionHandlingTests)
    for (int r = 0; r < 9; r++)
    {
        var r1 = r;
        th = th.Where(t => Z3Methods.Distinct(
            t.Cells[r1 * 9 + 0], t.Cells[r1 * 9 + 1], t.Cells[r1 * 9 + 2],
            t.Cells[r1 * 9 + 3], t.Cells[r1 * 9 + 4], t.Cells[r1 * 9 + 5],
            t.Cells[r1 * 9 + 6], t.Cells[r1 * 9 + 7], t.Cells[r1 * 9 + 8]));
    }
    for (int c = 0; c < 9; c++)
    {
        var c1 = c;
        th = th.Where(t => Z3Methods.Distinct(
            t.Cells[0 * 9 + c1], t.Cells[1 * 9 + c1], t.Cells[2 * 9 + c1],
            t.Cells[3 * 9 + c1], t.Cells[4 * 9 + c1], t.Cells[5 * 9 + c1],
            t.Cells[6 * 9 + c1], t.Cells[7 * 9 + c1], t.Cells[8 * 9 + c1]));
    }
    for (int b = 0; b < 9; b++)
    {
        var b1 = b;
        var start = (b1 / 3) * 27 + (b1 % 3) * 3;
        th = th.Where(t => Z3Methods.Distinct(
            t.Cells[start],      t.Cells[start + 1],  t.Cells[start + 2],
            t.Cells[start + 9],  t.Cells[start + 10], t.Cells[start + 11],
            t.Cells[start + 18], t.Cells[start + 19], t.Cells[start + 20]));
    }
    return th;
}

Console.WriteLine("BuildArrayTheorem pret : 81 domaines + 27 unites, tout en boucles");

BuildArrayTheorem pret : 81 domaines + 27 unites, tout en boucles

// Barreau 2 : resolution du puzzle temoin en mode Constants
var sw2 = Stopwatch.StartNew();
var ctx2 = new Z3Context { DefaultCollectionHandling = CollectionHandling.Constants };
var th2 = BuildArrayTheorem(ctx2);
for (int k = 0; k < 81; k++)
{
    if (WIKI_PUZZLE[k] != 0)
    {
        var k1 = k; var v1 = WIKI_PUZZLE[k];
        th2 = th2.Where(t => t.Cells[k1] == v1);
    }
}
var sol2 = th2.Solve();
sw2.Stop();

Console.WriteLine($"Mode Constants : resolution en {sw2.ElapsedMilliseconds} ms");
DisplayFlat(sol2.Cells.ToArray(), "Solution (mode Constants)");

Mode Constants : resolution en 72 ms
--- Solution (mode Constants) ---
-------------------------
| 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 | 
-------------------------

Interprétation 2 — boucles et closures remplacent la réflexion

Comparez les deux barreaux sur le même geste « chaque cellule entre 1 et 9 » :

• rung 1 : Expression.Property(t, "Cell" + i + j) — réflexion sur des noms, hors du DSL ;
• rung 2 : th.Where(s => s.Cells[i1 * 9 + j1] > 0 && ...) — une expression C# ordinaire, dans le DSL, dans une boucle.

L’indice reste aplati (i * 9 + j) — la grille est un List<int> de 81 éléments, la géométrie est arithmétique modulaire dans les contraintes de blocs (start, +9, +18). Notez la capture de closure (var i1 = i) : sans cette copie locale, toutes les lambdas referenceraient la même variable de boucle et le théorème résolu serait faux — c’est le piège classique du rung, celui que la sortie du notebook 02 de la série SMT documente aussi.

La classe modèle est passée de 220 lignes (81 propriétés) à 4 lignes (1 collection).

// Barreau 2 (bis) : le meme theoreme, le meme puzzle, en mode Array
var sw2b = Stopwatch.StartNew();
var ctx2b = new Z3Context { DefaultCollectionHandling = CollectionHandling.Array };
var th2b = BuildArrayTheorem(ctx2b);
for (int k = 0; k < 81; k++)
{
    if (WIKI_PUZZLE[k] != 0)
    {
        var k1 = k; var v1 = WIKI_PUZZLE[k];
        th2b = th2b.Where(t => t.Cells[k1] == v1);
    }
}
var sol2b = th2b.Solve();
sw2b.Stop();

Console.WriteLine($"Mode Array : resolution en {sw2b.ElapsedMilliseconds} ms");
DisplayFlat(sol2b.Cells.ToArray(), "Solution (mode Array)");
Console.WriteLine($"Identique a la solution Constants : {sol2.Cells.SequenceEqual(sol2b.Cells)}");

Mode Array : resolution en 43 ms
--- Solution (mode Array) ---
-------------------------
| 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 | 
-------------------------
Identique a la solution Constants : True

Interprétation 3 — Constants vs Array : deux front-ends, un même théorème

La même fonction BuildArrayTheorem a produit les deux solutions — le code utilisateur ne change pas d’une ligne entre les deux modes ; seul le réglage du contexte diffère. C’est la propriété que les tests du fork épingle : les deux front-ends d’indexation (nœud ArrayIndex pour int[], appel get_Item pour List<T>) doivent rester alignés en comportement.

La différence est sémantique côté Z3 : en mode Array la collection est un objet unique que le solveur contraint via la théorie des tableaux (Store/Select imbriqués) ; en mode Constants elle est éclatée en constantes plates. Pour un Sudoku, les deux convergent — sur des problèmes où la cardinalité ou les quantificateurs bornés comptent, le choix du mode devient un vrai levier de modélisation (la série SMT, notebook 05, creuse cet écart).

3. Barreau 3 — les tableaux imbriqués int[][] (commit 096a638)

Troisième marche, portée par le commit 096a638 (« feat: add nested int[][] array support », branche feature/list-collection-constants-mode) : le modèle peut désormais être un tableau de tableaux. Les artefacts sont SudokuGrid.cs et SudokuGridTheorem.cs :

public class SudokuGrid
{
    public int[][] Cells { get; set; } = new int[9][];
}

La cellule s’écrit g.Cells[row][col] — plus d’arithmétique i * 9 + j, plus de tableau à une dimension : le modèle a la forme de la grille.

// Barreau 3 : le modele jagged, forme de SudokuGrid.cs
public class SudokuGrid
{
    public int[][] Cells { get; set; } = new int[9][];
    public SudokuGrid()
    {
        for (int i = 0; i < 9; i++) Cells[i] = new int[9];
    }
}

// Le theoreme, forme de SudokuGridTheorem.cs
Theorem<SudokuGrid> BuildGridTheorem(Z3Context ctx)
{
    var th = ctx.NewTheorem<SudokuGrid>();

    // Domaines : g.Cells[row][col] entre 1 et 9
    for (int i = 0; i < 9; i++)
        for (int j = 0; j < 9; j++)
        {
            var (r, c) = (i, j);
            th = th.Where(g => g.Cells[r][c] >= 1 && g.Cells[r][c] <= 9);
        }

    // Unites : rangee, colonne, bloc — l'indice a deux dimensions, comme la grille
    for (int i = 0; i < 9; i++)
    {
        var row = i;
        th = th.Where(g => Z3Methods.Distinct(
            g.Cells[row][0], g.Cells[row][1], g.Cells[row][2],
            g.Cells[row][3], g.Cells[row][4], g.Cells[row][5],
            g.Cells[row][6], g.Cells[row][7], g.Cells[row][8]));
    }
    for (int j = 0; j < 9; j++)
    {
        var col = j;
        th = th.Where(g => Z3Methods.Distinct(
            g.Cells[0][col], g.Cells[1][col], g.Cells[2][col],
            g.Cells[3][col], g.Cells[4][col], g.Cells[5][col],
            g.Cells[6][col], g.Cells[7][col], g.Cells[8][col]));
    }
    for (int br = 0; br < 3; br++)
        for (int bc = 0; bc < 3; bc++)
        {
            var (R, C) = (br, bc);
            th = th.Where(g => Z3Methods.Distinct(
                g.Cells[R * 3][C * 3],     g.Cells[R * 3][C * 3 + 1],     g.Cells[R * 3][C * 3 + 2],
                g.Cells[R * 3 + 1][C * 3], g.Cells[R * 3 + 1][C * 3 + 1], g.Cells[R * 3 + 1][C * 3 + 2],
                g.Cells[R * 3 + 2][C * 3], g.Cells[R * 3 + 2][C * 3 + 1], g.Cells[R * 3 + 2][C * 3 + 2]));
        }
    return th;
}

Console.WriteLine("BuildGridTheorem pret : Cells[row][col], la forme de la grille");

BuildGridTheorem pret : Cells[row][col], la forme de la grille

// Barreau 3 : resolution du puzzle temoin sur le modele jagged
var sw3 = Stopwatch.StartNew();
var ctx3 = new Z3Context();
var th3 = BuildGridTheorem(ctx3);
for (int i = 0; i < 9; i++)
    for (int j = 0; j < 9; j++)
    {
        if (WIKI_PUZZLE[i * 9 + j] != 0)
        {
            var (r, c) = (i, j); var v = WIKI_PUZZLE[i * 9 + j];
            th3 = th3.Where(g => g.Cells[r][c] == v);
        }
    }
var sol3 = th3.Solve();
sw3.Stop();

Console.WriteLine($"Modele jagged : resolution en {sw3.ElapsedMilliseconds} ms");
DisplayNested(sol3.Cells, "Solution (int[][])");

var flat3 = new int[81];
for (int i = 0; i < 9; i++) for (int j = 0; j < 9; j++) flat3[i * 9 + j] = sol3.Cells[i][j];
Console.WriteLine($"Identique a la solution du barreau 2 : {sol2.Cells.SequenceEqual(flat3)}");

Modele jagged : resolution en 47 ms
--- Solution (int[][]) ---
-------------------------
| 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 | 
-------------------------
Identique a la solution du barreau 2 : True

Interprétation 4 — le modèle ressemble enfin à la grille

Le commit 096a638 fait passer l’expression de s.Cells[i1 * 9 + j1] à g.Cells[r][c]. Techniquement, le visitor du binding apprend à descendre dans les nœuds ArrayIndex imbriqués : g.Cells[r] est un premier tableau, [c] indexes le second — l’expression C# arbore deux niveaux que le binding compile en Select(Select(cells, r), c) côté SMT.

Le gain n’est pas cosmétique :

• les contraintes de blocs se lisent g.Cells[R*3][C*3] au lieu de start + 18 — la géométrie est dans les indices, plus dans l’arithmétique ;
• la sortie se parcourt comme une grille (sol3.Cells[i][j]) sans dé-aplatissement ;
• la classe modèle reflète la donnée réelle d’un Sudoku (une grille 9x9), pas son encodage linéarisé.

Les trois rungs démontrés résolvent le même puzzle — vérifié en sortie : les trois solutions coïncident. L’échelle ne change pas le moteur (c’est toujours le Z3 de Sudoku-12) ; elle change le coût d’expression du modèle.

4. Barreau 4 — int[,] : l’intention confrontée au code réel

La quatrième marche — les tableaux rectangulaires int[,] — est signalée comme la dernière évolution voulue du binding. Ce notebook l’atteste honnêtement plutôt qu’il ne la démontre : au 2026-09-06, int[,] comme type de modèle de théorème est absent du code du fork (scan exhaustif des 30 refs distantes : le motif int[,] n’apparaît dans aucun .cs du binding ; les seules occurrences de int[,] dans les notebooks de la série SMT sont des données de puzzle, pas des modèles — cf. notebook 05, indices déclarés int[,] puis convertis).

Ce qui existe déjà, on peut le voir tourner : la forme du nœud d’expression que le visitor devrait apprendre à router. Comparons les trois accès que C# compile différemment :

// Barreau 4 : confrontation en direct — trois acces, trois formes d'arbre d'expression
Expression<Func<int[][], int>> jaggedAccess = a => a[1][2];
Expression<Func<List<int>, int>> listAccess  = l => l[1];
Expression<Func<int[,],   int>> rectAccess   = g => g[1, 2];

Console.WriteLine("jagged  a[1][2]  : " + jaggedAccess.Body.NodeType + "  |  " + jaggedAccess.Body);
Console.WriteLine("list    l[1]     : " + listAccess.Body.NodeType + "  |  " + listAccess.Body);
Console.WriteLine("rect    g[1,2]   : " + rectAccess.Body.NodeType + "  |  " + rectAccess.Body);
Console.WriteLine();
Console.WriteLine("detail rect : " + rectAccess.Body.GetType().Name);
if (rectAccess.Body is MethodCallExpression call)
    Console.WriteLine("methode appelee : " + call.Method.Name);

jagged  a[1][2]  : ArrayIndex  |  a[1][2]
list    l[1]     : Call  |  l.get_Item(1)
rect    g[1,2]   : Call  |  g.Get(1, 2)

detail rect : InstanceMethodCallExpression2
methode appelee : Get

Interprétation 5 — chaque rung est un nœud d’expression routé

La sortie ci-dessus est l’explication du barreau manquant, lue dans le compilateur : les trois accès ne compilent pas vers la même forme. L’accès imbriqué a[1][2] et l’indexeur l[1] produisent des nœuds que le visitor du binding sait déjà traduire (c’est le barreau 2 — get_Item — et le barreau 3 — ArrayIndex imbriqué) ; l’accès rectangulaire g[1,2] produit une autre forme, celle que le visitor ne route pas encore.

Relue depuis la sortie, toute l’échelle prend son sens générique : un binding LINQ évolue en apprenant des nœuds d’expression. Chaque rung de l’histoire — propriétés (Member), collections indicées (Call get_Item), tableaux imbriqués (ArrayIndex imbriqué) — est un type de nœud que ExpressionVisitor a appris à compiler vers Z3. Le rung 4 attend son routage.

C’est la frontière honnête de ce notebook : il atteste le rung manquant (code scanné, nœud exhibé) sans le combler — l’implémenter serait une PR du fork Z3.Linq, pas un livrable pédagogique Sudoku.

// Barreau 4 : ce que la branche porte deja — la donnee 2D convertie vers le modele jagged
int[,] clues2D = new int[9, 9];
for (int i = 0; i < 9; i++)
    for (int j = 0; j < 9; j++)
        clues2D[i, j] = WIKI_PUZZLE[i * 9 + j];

var sw4 = Stopwatch.StartNew();
var ctx4 = new Z3Context();
var th4 = BuildGridTheorem(ctx4);
for (int i = 0; i < 9; i++)
    for (int j = 0; j < 9; j++)
    {
        if (clues2D[i, j] != 0)
        {
            var (r, c) = (i, j); var v = clues2D[i, j];
            th4 = th4.Where(g => g.Cells[r][c] == v);
        }
    }
var sol4 = th4.Solve();
sw4.Stop();

Console.WriteLine($"Donnee int[,] -> modele jagged : resolution en {sw4.ElapsedMilliseconds} ms");
DisplayNested(sol4.Cells, "Solution (indices 2D, modele jagged)");

Donnee int[,] -> modele jagged : resolution en 51 ms
--- Solution (indices 2D, modele jagged) ---
-------------------------
| 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 | 
-------------------------

Interprétation 6 — la donnée 2D existe déjà, c’est le modèle qui attend son rung

Le pont pratiqué aujourd’hui : déclarer les indices en int[,] (la forme naturelle d’une grille de données — celle du notebook 05 de la série SMT, celle de l’exercice Z3 de Sudoku-13), puis les verser dans le modèle jagged. La conversion coûte une double boucle de lecture ; le théorème, lui, reste du barreau 3.

Quand le rung 4 existera dans le fork, cette cellule perdra sa boucle de conversion et la classe SudokuGrid déclarera int[,] Cells — même moteur, même solveur, un nœud d’expression de plus routé. L’échelle est ouverte vers le haut.

5. Exercices

Exercice 1 — 16x16 : mesurer la marche du rung 1

Objectif : un Sudoku 16x16 (valeurs 1 à 16, blocs 4x4) sur le rung de votre choix. Estimez d’abord sur papier ce que coûterait le rung 1 : combien de propriétés, combien de contraintes d’unité explicites ? Puis implémentez-le sur un rung indicé (barreau 2 ou 3) et comparez votre estimation au code réellement écrit.

Indice : réutilisez BuildGridTheorem en paramétrant la taille (9 -> 16, blocs 3 -> 4).

// EXERCICE : Sudoku 16x16 sur un rung indicie
// TODO etudiant : generaliser BuildGridTheorem a une taille N (N=16, blocs de 4)
// puis construire le theoreme et poser quelques indices avant de resoudre.
// Etape 1 : ecrire Theorem<TGrid> BuildGridTheoremN<TGrid>(Z3Context ctx, int n) ou equivalent
// Etape 2 : poser 4 a 6 indices valides d'un 16x16
// Etape 3 : resoudre et afficher

Console.WriteLine("Exercice a completer : Sudoku 16x16 — le rung 1 exigerait 256 proprietes ; combien de lignes avec le votre ?");

Exercice a completer : Sudoku 16x16 — le rung 1 exigerait 256 proprietes ; combien de lignes avec le votre ?

Exercice 2 — Constants vs Array : mesurer l’écart sur trois puzzles

Objectif : chronométrer les deux modes (CollectionHandling.Constants et .Array) sur trois puzzles de difficultés différentes (le témoin ci-dessus, une grille presque vide, une grille presque pleine), et rapporter les temps dans un tableau. Formulez une hypothèse : lequel des deux régimes favorise quel mode ?

Indice : pour générer les grilles, retirez aléatoirement des indices du puzzle témoin (grille presque vide) ou partez de la solution et retirez-en peu (grille presque pleine).

// EXERCICE : Constants vs Array sur trois puzzles
// TODO etudiant : construire les trois grilles, resoudre chacune dans les deux modes, chronometrer.
// Etape 1 : grille presque vide (<= 10 indices) et grille presque pleine (>= 50 indices)
// Etape 2 : pour chaque grille : BuildArrayTheorem + indices, dans un contexte Constants puis dans un contexte Array
// Etape 3 : rapporter les 6 temps dans un tableau + une phrase d'interpretation

var mesuresExercice2 = new List<string>();  // TODO etudiant : remplir ("grille x mode : y ms")
Console.WriteLine("Exercice a completer : 6 mesures a rapporter (3 grilles x 2 modes).");

Exercice a completer : 6 mesures a rapporter (3 grilles x 2 modes).

Exercice 3 — prédire la forme du nœud, puis vérifier

Objectif : sans l’exécuter, prédire ce qu’affiche Expression<Func<int[,,], int>> c = a => a[1, 2, 3]; (tableau tridimensionnel) : quel NodeType, quelle forme de corps ? Notez votre prédiction, puis vérifiez.

Indice : généralisez la lecture de la section 4 — que fait le compilateur quand il y a plus de deux indices ?

// EXERCICE : le nœud du tableau 3D
// TODO etudiant : noter la prediction ici (en commentaire), puis decommenter et executer.
// Prediction : ...
// Expression<Func<int[,,], int>> cubeAccess = a => a[1, 2, 3];
// Console.WriteLine(cubeAccess.Body.NodeType + "  |  " + cubeAccess.Body);

Console.WriteLine("Exercice a completer : ecrire la prediction, puis decommenter les deux lignes pour verifier.");

Exercice a completer : ecrire la prediction, puis decommenter les deux lignes pour verifier.

Exercice 4 — Sudoku-X : étendre le théorème jagged

Objectif : le Sudoku-X ajoute deux contraintes d’unité : les deux diagonales principales doivent aussi contenir 1 à 9. Étendez BuildGridTheorem en BuildGridTheoremX (une dizaine de lignes) et résolvez le puzzle témoin — le Sudoku-X a-t-il encore une solution avec ces indices ?

Indice : diagonale principale g.Cells[k][k], anti-diagonale g.Cells[k][8 - k] — deux Z3Methods.Distinct de plus. La réponse à la question finale n’est pas « oui » ; vérifiez ce que renvoie Solve() quand le problème devient insatisfiable.

// EXERCICE : Sudoku-X sur le modele jagged
// TODO etudiant : reprendre BuildGridTheorem et ajouter les deux unites diagonales.
// Etape 1 : BuildGridTheoremX (copie + deux Distinct)
// Etape 2 : poser les indices du puzzle temoin et resoudre
// Etape 3 : si Solve() renvoie null, expliquer pourquoi dans un Console.WriteLine

Console.WriteLine("Exercice a completer : etendre le theoreme aux diagonales et tester la satisfiabilite.");

Exercice a completer : etendre le theoreme aux diagonales et tester la satisfiabilite.

Conclusion — ce que raconte l’échelle

Les quatre barreaux ne changent ni le solveur, ni le problème : c’est le Z3 de Sudoku-12 à chaque marche, sur le même puzzle témoin, avec trois solutions identiques vérifiées en sortie. Ce qui change de rung en rung, c’est le coût d’expression du modèle :

Rung	Classe modèle (9x9)	Contraintes écrites	Forme compilée
1 — propriétés	220 lignes, 81 propriétés	réflexion + 27 Distinct explicites	nœuds Member
2 — collections	4 lignes, List<int>	boucles + closures	Call get_Item / constantes plates ou Store/Select
3 — jagged	4 lignes, int[][]	boucles, indices à deux dimensions	ArrayIndex imbriqués
4 — int[,]	—	—	appel Get(i, j) exhibé en section 4, non routé à ce jour

La leçon transférable dépasse le binding : une API déclarative gagne ses marches une forme d’expression à la fois. Chaque rung de Z3.Linq est un type de nœud que le visitor a appris à compiler vers SMT — et le rung manquant se diagnostique exactement ainsi : exhiber le nœud, montrer qu’aucun routage ne le prend.

Pour aller plus loin : la série SymbolicAI/SMT/Z3-Linq2Z3/ — en particulier 02 : Théorème vs Arrays (les deux stratégies de modélisation), 03 : comparaison des modes et 05 : tableaux imbriqués et grilles 2D (l’encodage Store/Select imbriqué côté Z3 brut).

Provenance et ancrages

• Articles fondateurs (Bart De Smet, 2009, conservés sur archive.org, re-déposés dans le fork sous docs/blogs/) : Exploring the Z3 Theorem Prover (15 avril 2009) · LINQ to the Unexpected (19 avril 2009) · Theorem Solving on Steroids (27 septembre 2009).
• Binding : fork MyIntelligenceAgency/Z3.Linq (fork de endjin/Z3.Linq), sous-module SymbolicAI/SMT/Z3.Linq, pointeur 20984bf — les exécutions de ce notebook utilisent son dossier .deploy/ préassemblé.
• Artefacts cités : solutions/Z3.Linq.Examples/Sudoku/SudokuTable.cs (rung 1, 81 propriétés) · SudokuTheorem.cs (contraintes par réflexion "Cell{0}{1}") · SudokuGrid.cs + SudokuGridTheorem.cs (rung 3) · ListCollectionTests.cs (alignement des deux front-ends d’indexation).
• Commits et branches : 096a638 « feat: add nested int[][] array support » (rung 3) · branche feature/list-collection-constants-mode (rung 2).
• Références : épic #1206 (piste Z3.Linq) · #14169 (posture de fork amont) · #6300 (nomenclature Z3-Linq-primary) · #5081 (convention d’accrétion Sudoku : la lettre colle au numéro).

---

Sudoku-12 Z3 C# | Index | Sudoku-13 Automates symboliques >>