---

Navigation : << Sudoku-12 Z3 C# | Index | Sudoku-14 Retour d’expérience >>

---

Sudoku-13 : Le Sudoku comme Regex Symbolique - l’échelle Conway -> BREX/Rex -> RE

Ce notebook reprend et aboutit une tentative personnelle de 2020 : représenter un Sudoku comme un grand regex symbolique où les contraintes de lignes, colonnes et blocs se combinent par intersection (Ligne & Colonne & Bloc), puis demander à un solveur d’en extraire une grille-témoin.

La tentative de 2020 a buté sur deux murs réels - tous deux des murs de l’automate (déterminisation explosive + témoin capé). La chaîne moderne change de moteur : les opérateurs de surface & / ~ se compilent vers la théorie des chaînes de Z3, qui ne construit aucun produit d’automates et n’a aucun plafond de témoin. Les deux murs de 2020 disparaissent. Restait le 9x9 : longtemps unknown (au-delà d’une minute d’attente) quand le tous-distincts est fondu en un seul automate d’intersection (re.inter / str.in_re). La pièce manquante - l’élément de syntaxe entrevu en 2020 - tient en un mot : chaque conjonct d’appartenance .*d.* a une primitive native dans la théorie des chaînes, str.contains. Émise ainsi (un str.contains par chiffre) plutôt que fondue en re.inter, la même intersection & d’appartenances fait atterrir la grille 9x9 complète - témoin réel, valide, en ~53 s (binding .NET ; ~12 s en z3-py). Zéro inégalité : le regex se suffit à lui-même.

La thèse en une phrase

Un Sudoku se laisse décrire et résoudre comme une intersection de contraintes régulières. Décrire (reconnaître une grille valide) et produire (résoudre le puzzle) restent deux métiers - RE# excelle au premier, Z3 au second - mais le regex & ne s’arrête pas à la reconnaissance : porté vers la théorie des chaînes de Z3 dans la bonne forme d’émission (chaque .*d.* en str.contains natif, pas fondu en re.inter), il atterrit la grille 9x9 complète, sans une seule inégalité. Ce qui décide n’est ni le moteur ni le substrat, c’est la forme d’émission du même & d’appartenances : produit d’automates (sature) vs primitive native (atterrit).

Comment lire ce carnet. Le fil principal (sections 1 à 8) raconte une escalade : trois barreaux pour vérifier une grille (le PCRE monstre, BREX/Rex, RE#), puis le saut de vérifier à résoudre avec Z3 — où l’on découvre en mesurant que la forme d’émission de la contrainte, pas le moteur, décide de ce qui atterrit. Chaque section ne suppose que la précédente ; trois exercices jalonnent le parcours.

Deux annexes lettrées approfondissent sans interrompre le récit : annexe A (les cadres théoriques de Veanes : M2L-str et décomposition monadique), annexe B (les tableaux consolidés du banc d’essai complet). Les annexes S10 et S11, en fin de carnet, ouvrent deux ponts indépendants vers les moteurs natifs (Z3 en SMT-LIB direct, BDD via PythonNet).

1. Introduction : un Sudoku comme grand regex ?

En 2020, l’auteur entreprenait de représenter un Sudoku non pas comme un monstre PCRE à backtracking (le folklore Perl du “Sudoku en un regex”, barreau 1 ci-dessous), mais comme une chaîne déclarative tractable où :

• chaque contrainte (ligne, colonne, bloc) est un regex symbolique ;
• les contraintes se combinent par intersection (&) et complément (~) ;
• l’intersection compile vers un terme SMT ;
• un solveur SMT (Z3) en extrait un modèle = la grille solution (un témoin).

Le timing n’était pas un hasard. Après le binding LINQ-to-Z3 (2018), deux publications du groupe Veanes/MSR venaient d’annoncer la pièce qui semblait manquante : SRM (“Symbolic Regex Matcher”, TACAS 2019) portait un moteur à dérivées symboliques, et dZ3 (“Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints”, PLDI 2021) montrait que les combinaisons booléennes de regex - exactement Ligne & Colonne & Bloc - se résolvent efficacement via Z3, là où les méthodes antérieures explosaient. Sur le papier, c’était le bon moment.

Trois façons de “résoudre un Sudoku avec des regex” (à ne pas confondre)

Paradigme	Qui fait la recherche	Atterrit la grille ?
Conway / backtracking ((?R), déroulé Griffis)	le moteur regex lui-même	fragile (timeout / faux négatif)
SFA / produit d’automates (Automata.NET 2020 : Rex + SFAz3)	produit de DFA + témoin SFAz3	toys oui ; grille -> mur 1 (explosion) + mur 2 (cap #6)
regex -> théorie des chaînes SMT directe (fork RegexToSMTConverter)	le solveur de chaînes Z3, aucun automate matérialisé	4x4 complet ; 9x9 complet (cf. infra)

Ce notebook raconte honnêtement cette histoire : ses deux murs de 2020, le changement de moteur qui les fait tomber, puis la dernière marche - le 9x9 - que franchit la forme d’émission de l’intersection : fondue en re.inter, l’appartenance sature ; éclatée en str.contains natif, elle atterrit le 9x9 complet.

Reconnaître != résoudre

Approche	RESOUDRE (produire le témoin)	VERIFIER (valider une grille)
Folklore PCRE (backtracking, barreau 1)	détour de backtracking, illisible	monstrueux
2020 - AutomataDotNet (BREX/Rex + SFAz3)	muré : cap témoin ~21 char (#6) + explosion du produit	intersection -> DFA, mais explose
Moderne - &/~ -> théorie des chaînes Z3	témoin non capé, sans produit d’automates ; atterrit la grille (4x4 et 9x9)	(oui)
2025 - RE#	aucun témoin (recognition-only)	temps linéaire
Z3 Distinct (81 entiers)	résolveur de production (~38 ms)	-

Les deux murs de 2020 étaient des murs de l’automate : ils tombent dès qu’on change de moteur (produit de DFA -> théorie des chaînes Z3). La voie symbolique atterrit réellement une grille - 4x4 complète, et 9x9 complète - sans jamais quitter l’appartenance régulière. La leçon n’est pas “le regex est le mauvais outil” mais, plus fine : ce qui décide n’est ni le moteur ni le substrat, c’est la forme d’émission du même & d’appartenances. Fondu en un produit d’automates (re.inter / str.in_re), il sature à l’échelle du 9x9 ; éclaté en la primitive native str.contains (un par chiffre, soit exactement .*d.*), il atterrit la grille 9x9 complète (~53 s en .NET), sans une seule inégalité. Le bon outil suit la forme du problème - et le regex, bien émis, est cet outil.

2. Barreau 1 - le monstre PCRE : “le Sudoku en un seul regex”

Le folklore Perl du “Sudoku en un seul regex” remonte aux PerlMonks du milieu des années 2000 (ikegami, 2005 ; plus tard le module pur-regex Regexp::Sudoku d’Abigail). L’idée : le backtracking du moteur regex est un moteur de recherche, et la grille devient un unique match potentiel.

Ce tour de force existe en deux formes réelles (souvent confondues) :

• la forme récursive ((?R) / (?0)) : le motif s’auto-invoque pour explorer la grille. Elle est non régulière et hors de portée de .NET (System.Text.RegularExpressions ne fait pas de récursion de motif) ;
• la forme déroulée : les 81 cases sont écrites explicitement (backreferences + lookaheads, sans (?R)), lignée Aron Griffis (2007), domaine public. Elle tourne sur tout moteur à backtracking, .NET compris.

Dans les deux cas, le pattern est un monstre illisible, inversement pédagogique, et non généralisable - du folklore de concours, pas une méthode. La forme déroulée est celle que nous générons et exécutons réellement en section 8 ; le tronceau ci-dessous en est extrait (un troncage de l’artefact réel sauvegardé dans assets/sudoku-unrolled.regex.txt), pas un fragment reconstruit à la main.

// Le VRAI monstre regex (forme deroulee, lignee Conway/folklore PCRE) genere en section 8
// et sauvegarde dans assets/sudoku-unrolled.regex.txt. On en affiche un TRONCAGE : tete + queue,
// extraits du fichier réel (pas un fragment reconstruit à la main).
using System;
using System.IO;
using System.Linq;

string[] candidats = {
    "assets/sudoku-unrolled.regex.txt",
    "MyIA.AI.Notebooks/Sudoku/assets/sudoku-unrolled.regex.txt",
    Path.Combine("..", "Sudoku", "assets", "sudoku-unrolled.regex.txt")
};
string chemin = candidats.FirstOrDefault(File.Exists);

if (chemin == null) {
    Console.WriteLine("(artefact assets/sudoku-unrolled.regex.txt absent - il est (re)genere en section 8)");
} else {
    string monstre = File.ReadAllText(chemin);
    int n = monstre.Length;
    string tete  = monstre.Substring(0, Math.Min(420, n));
    string queue = n > 720 ? monstre.Substring(n - 300) : "";
    Console.WriteLine($"Monstre regex deroule (forme exacte, {n} caracteres) - TRONCAGE de {Path.GetFileName(chemin)} :");
    Console.WriteLine("--- tete (420 premiers caracteres) -------------------------------");
    Console.WriteLine(tete);
    Console.WriteLine($"--- [... {n - 720} caracteres omis ...] --------------------------");
    Console.WriteLine(queue);
    Console.WriteLine("------------------------------------------------------------------");
    Console.WriteLine();
    Console.WriteLine("-> Backtracking PCRE detourne en moteur de recherche : ca 'tourne' (section 8),");
    Console.WriteLine("   mais l'unicite encodee en lookaheads/backrefs est illisible. Ce n'est PAS");
    Console.WriteLine("   la representation declarative que nous cherchons (intersection -> Z3).");
}

Monstre regex deroule (forme exacte, 13515 caracteres) - TRONCAGE de sudoku-unrolled.regex.txt :
--- tete (420 premiers caracteres) -------------------------------
\A

\d*(\d)
(?!(?:.*\n)+(?:.{10}){0}\1\b)
(?!\d*\ (?:.{10})*?\1\b)
(?!\d*\ (?:.{10}){0,1}\1\b)
(?!(?:.*\n){1,2}(?:.{30}){0}(?:.{10}){0,2}\1\b)
\d*\s+

\d*(?!\1)
(\d)
(?!(?:.*\n)+(?:.{10}){1}\2\b)
(?!\d*\ (?:.{10})*?\2\b)
(?!\d*\ (?:.{10}){0,0}\2\b)
(?!(?:.*\n){1,2}(?:.{30}){0}(?:.{10}){0,2}\2\b)
\d*\s+

\d*(?!\1|\2)
(\d)
(?!(?:.*\n)+(?:.{10}){2}\3\b)
(?!\d*\ (?:.{10})*?\3\b)
(?!(?:.*\n){1,2}(?:.{30}){0}(?:.{10}){0,2}
--- [... 12795 caracteres omis ...] --------------------------
|\70|\71|\72|\73|\74|\75|\76|\77|\78|\79)
(\d)
(?!(?:.*\n)+(?:.{10}){7}\80\b)
(?!\d*\ (?:.{10})*?\80\b)
(?!\d*\ (?:.{10}){0,0}\80\b)
\d*\s+

\d*(?!\9|\18|\27|\36|\45|\54|\61|\62|\63|\70|\71|\72|\73|\74|\75|\76|\77|\78|\79|\80)
(\d)
(?!(?:.*\n)+(?:.{10}){8}\81\b)
(?!\d*\ (?:.{10})*?\81\b)
\d*\s+

\Z

------------------------------------------------------------------

-> Backtracking PCRE detourne en moteur de recherche : ca 'tourne' (section 8),
   mais l'unicite encodee en lookaheads/backrefs est illisible. Ce n'est PAS
   la representation declarative que nous cherchons (intersection -> Z3).

Interprétation : le monstre PCRE = l’anti-modèle

Ce monstre démontre par l’absurde que détourner le backtracking d’un moteur regex pour faire de la recherche conduit à une représentation illisible. La contrainte d’unicité Sudoku n’est pas naturelle en PCRE : elle s’exprime en empilant des lookaheads négatifs sur les cellules déjà posées. La forme déroulée tourne (section 8) mais reste illisible et, on le verra, non portable d’un moteur à l’autre ; la forme récursive (?R) ne tourne même pas en .NET.

La bonne représentation, c’est l’intersection déclarative de contraintes (Ligne & Colonne & Bloc) - portée proprement par RE# pour la reconnaissance (sections 4-5) et par Z3 pour la production du témoin (section 6). C’est exactement ce que cherchait l’approche 2020.

3. Barreau 2 - La tentative 2020 : BREX, Rex et le mur

En 2020, l’auteur s’appuie sur la chaîne d’outils symboliques de Margus Veanes (AutomataDotNet) pour réaliser l’intersection déclarative. Deux briques existaient, vérifiées par lecture du source au commit 0242132f :

1. L’intersection existait - via BREX (Boolean combinations of Regular EXpressions, fichiers BREX.cs, BREXManager.cs). Mais c’était une API builder C#, pas un opérateur & de surface dans une chaîne :

var man  = new BREXManager();
var like1 = man.MkLike(@"%[ab]_____");
var like2 = man.MkLike(@"%[bc]_____");
var and   = man.MkAnd(like1, like2);   // l'intersection : une MÉTHODE, pas un '&' dans la chaîne
var dfa   = and.Optimize();

2. Le témoin Z3 existait - via la lignée Rex (RegexToSMTConverter.cs) : génération d’un membre/témoin d’un regex par SMT. C’est ce chemin qui a buté sur la troncature à 21 caractères.

Les deux murs réels (vérifiés dans les tests)

Mur	Preuve dans le source	Conséquence
Explosion d’états	BREXTests.cs porte les commentaires //fails due to timeout et //fails due to too many states - l’intersection de deux MkLike de 8-9 underscores seulement fait exploser le DFA via Optimize()	L’intersection symbolique est trop chère à déterminiser
Cap du témoin à 21 caractères	Issue upstream AutomataDotNet/Automata#6 (créée le 2020-12-07, toujours 0 réponse) : le chemin SFAz3+Z3 tronque le modèle	On ne peut pas produire une grille-témoin complète

Le bloc C# ci-dessus illustre la forme de l’approche 2020 : un spaghetti de builders (MkAnd(MkLike(...), ...)) et de strings, pas encore la chaîne monolithique élégante - et, surtout, barre par les deux murs ci-dessus. Le notebook ne rejoue pas ce code (AutomataDotNet est un projet Microsoft abandonné) : il en montre le squelette, puis passe au fork moderne (section 6b) qui, lui, exécute la voie regex -> théorie des chaînes.

Synthèse : deux murs, tous deux des murs de l’automate

L’approche 2020 n’était pas le folklore PCRE : l’intuition déclarative par intersection était fondue et contemporaine des travaux de Veanes. Mais la forme (builder C# MkAnd(MkLike(...), MkLike(...))) était un spaghetti, et deux murs réels l’ont bloquée :

1. l’intersection symbolique explose à la déterminisation (produit de DFA) ;
2. le chemin témoin SFAz3 -> Z3 est capé à ~21 caractères (#6).

Ces deux murs ont la même racine : on passe par la matérialisation d’un automate (déterminisation, puis extraction de témoin par ce chemin). Deux réparations, deux registres :

• pour la reconnaissance, RE# (section 4) rend l’intersection linéaire sans déterminisation exponentielle ;
• pour la production de témoin, la chaîne moderne (section 6b) compile &/~ vers la théorie des chaînes de Z3 : plus de produit d’automates (donc plus le mur 1) et plus de cap (mur 2 levé). Mais la difficulté ne s’évapore pas - elle migre dans le solveur de chaînes, comme on le mesurera.

4. Barreau 3 - RE# (2025) : la reconnaissance enfin tractable

RE# (NuGet Resharp, engine F#/.NET, MIT) étend la syntaxe System.Text.RegularExpressions avec trois opérateurs first-class :

• & : intersection (A & B reconnaît les mots acceptés par A ET par B) ;
• ~ : complément (~A reconnaît tout ce que A ne reconnaît pas) ;
• _ : wildcard universel.

Crucialement, RE# est non-backtracking et compile vers des automates dont la reconnaissance est temps linéaire - grâce à la finitude des dérivées symboliques (formalisée en Lean, cf section références). L’intersection de deux RE# ne déterminise pas de manière exponentielle : c’est précisément le mur 1 de 2020 qui tombe.

Caveat honnête : RE# est recognition-only. Il reconnaît (valide) ; il ne génère aucun témoin. Pour produire une grille, il faudra Z3 (section 6).

Note technique (environnement) : Resharp est un package NuGet standard (non modifié), mais #r "nuget: Resharp" ne suffit pas sous le kernel .net-csharp : le restore aboutit, puis RE# échoue à l’exécution avec FileNotFoundException: FSharp.Core, Version=10.0.0.0 - le kernel ne lie pas le runtime F# via une référence NuGet. On charge donc les DLL par chemin relatif vers un dossier .deploy committé dans le dépôt (SymbolicAI/SMT/Resharp/.deploy/ : Resharp.dll, Resharp.Runtime.dll et surtout FSharp.Core.dll 10.x, assembly 10.0.0.0). Résultat : reproductible après un simple clone, hors-ligne, sans aucun chemin utilisateur code en dur.

// RE# via DLL in-repo (.deploy, portable) : pas de #r "nuget:" sous papermill, et plus aucun chemin utilisateur code en dur.
// Resharp + Resharp.Runtime (net8.0) + FSharp.Core 10.x (assembly 10.0.0.0) co-localises dans le dossier .deploy committe ;
// chemin relatif au notebook, reproductible sur toute machine. Le kernel .net-csharp tourne sous net8.0.
#r "../SymbolicAI/SMT/Resharp/.deploy/FSharp.Core.dll"
#r "../SymbolicAI/SMT/Resharp/.deploy/Resharp.Runtime.dll"
#r "../SymbolicAI/SMT/Resharp/.deploy/Resharp.dll"
using System.Diagnostics;

// Smoke test : l'INTERSECTION & est first-class dans UNE chaîne. C'est l'operateur
// qui encode la contrainte de ligne Sudoku (section suivante). On le demontre ici
// en combinant 2 puis 3 contraintes d'inclusion dans la même expression.
var sw = Stopwatch.StartNew();
var has5And7 = new Resharp.Regex(@".*5.*&.*7.*");          // contient un 5 ET un 7
var has123   = new Resharp.Regex(@".*1.*&.*2.*&.*3.*");    // contient 1, 2 ET 3 (3-way)
sw.Stop();
Console.WriteLine($"RE# compile en {sw.ElapsedMilliseconds} ms (premier appel, JIT inclus).");
Console.WriteLine($"'527' contient 5 et 7     : {(has5And7.Matches("527").Length > 0 ? "oui" : "non")}");
Console.WriteLine($"'521' contient 5 et 7     : {(has5And7.Matches("521").Length > 0 ? "oui" : "non")}");
Console.WriteLine($"'123456789' a 1, 2 et 3   : {(has123.Matches("123456789").Length > 0 ? "oui" : "non")}");
Console.WriteLine($"'456789' a 1, 2 et 3      : {(has123.Matches("456789").Length > 0 ? "oui" : "non")}");
Console.WriteLine();
Console.WriteLine("RE# supporte aussi le complement ~ et le wildcard _ (first-class, documentes");
Console.WriteLine("par le moteur). Nous nous appuyons ici sur l'INTERSECTION &: c'est elle qui");
Console.WriteLine("encode de maniere robuste la contrainte de ligne Sudoku ci-dessous.");

RE# compile en 209 ms (premier appel, JIT inclus).
'527' contient 5 et 7     : oui
'521' contient 5 et 7     : non
'123456789' a 1, 2 et 3   : oui
'456789' a 1, 2 et 3      : non

RE# supporte aussi le complement ~ et le wildcard _ (first-class, documentes
par le moteur). Nous nous appuyons ici sur l'INTERSECTION &: c'est elle qui
encode de maniere robuste la contrainte de ligne Sudoku ci-dessous.

Interprétation : RE# valide, ne résout pas

RE# rend l’intersection (&) et le complément (~) first-class dans une chaîne unique, compilée en temps linéaire. C’est précisément le barreau intermédiaire qui manquait en 2020 : fini le spaghetti builder MkAnd(MkLike(...)), fini l’explosion DFA.

Mais notons le caveat déjà mentionné : RE# répond matche ou ne matche pas. Il ne dit pas quelle chaîne satisferait le pattern. C’est un vérificateur, pas un résolveur.

5. RE# vérificateur d’une ligne Sudoku remplie

Encodons la contrainte de ligne d’un Sudoku comme une intersection RE# :

Une ligne valide = exactement 9 chiffres 1-9 ([1-9]{9}) ET elle contient un 1 ET un 2 … ET un 9.

Soit, littéralement :

[1-9]{9} & .*1.* & .*2.* & .*3.* & .*4.* & .*5.* & .*6.* & .*7.* & .*8.* & .*9.*

Cette intersection de 10 regex est exactement le type d’opération qui faisait exploser le DFA en 2020 (BREXTests.cs : “//too many states” sur 8-9 underscores). Avec RE#, elle compile et s’exécute en temps linéaire.

using System.Diagnostics;
// La contrainte de ligne Sudoku comme intersection RE# (10 sous-regex).
// En 2020 cette intersection explosait le DFA ; RE# la compile en temps lineaire.
var sw = Stopwatch.StartNew();
var ligneValide = new Resharp.Regex(
    @"[1-9]{9}&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*");
sw.Stop();
Console.WriteLine($"Contrainte de ligne (10-way intersection) compilee en {sw.ElapsedMilliseconds} ms.");

void VerifierLigne(string ligne, string attendu)
{
    bool ok = ligneValide.Matches(ligne).Length > 0;
    string verdict = ok ? "VALIDE" : "invalide";
    Console.WriteLine($"  '{ligne}' -> {verdict}  (attendu : {attendu}) {(ok == (attendu == "VALIDE") ? "[OK]" : "[ECHEC]")}");
}

Console.WriteLine("\nLignes valides (permutations de 1..9) :");
VerifierLigne("123456789", "VALIDE");
VerifierLigne("987654321", "VALIDE");
VerifierLigne("534678912", "VALIDE");
Console.WriteLine("\nLignes invalides :");
VerifierLigne("123456788", "invalide");   // doublon (8 deux fois)
VerifierLigne("12345678",  "invalide");   // trop court
VerifierLigne("112345678", "invalide");   // doublon (1 deux fois)
VerifierLigne("123456780", "invalide");   // 0 interdit

Contrainte de ligne (10-way intersection) compilee en 35 ms.

Lignes valides (permutations de 1..9) :
  '123456789' -> VALIDE  (attendu : VALIDE) [OK]
  '987654321' -> VALIDE  (attendu : VALIDE) [OK]
  '534678912' -> VALIDE  (attendu : VALIDE) [OK]

Lignes invalides :
  '123456788' -> invalide  (attendu : invalide) [OK]
  '12345678' -> invalide  (attendu : invalide) [OK]
  '112345678' -> invalide  (attendu : invalide) [OK]
  '123456780' -> invalide  (attendu : invalide) [OK]

Interprétation : RE# vérifie en O(n), linéaire

La contrainte de ligne - une intersection de 10 regex - compile et s’exécute en temps linéaire. C’est le mur 1 de 2020 qui tombe : la même opération qui faisait exploser le DFA (//too many states) est désormais tractable.

Ce vérificateur reconnaît une ligne valide. Appliqué à chacune des 9 lignes d’une grille remplie, il valide la grille entière (après extraction des colonnes et blocs, mêmes contraintes). Mais il ne produit toujours aucune grille : donnez-lui un puzzle vide, il ne saura pas le remplir.

Exercice 1 : une contrainte d’intersection RE

Objectif : Écrivez un pattern RE# qui reconnaît une ligne Sudoku valide ET dans laquelle le chiffre 5 apparaît avant le 7 (sous-séquence 5 ... 7).

Indice : Composez par intersection la contrainte de ligne valide (ci-dessus) avec .*5.*7.* (un 5 puis, plus loin, un 7). RE# accepte l’imbrication libre de & dans une même chaîne.

Étape 1 : Définissez le pattern combine dans la cellule suivante. Une permutation comme 123456789 (5 avant 7) doit passer ; 987654321 (7 avant 5) doit échouer.

// EXERCICE : ligne Sudoku valide AVEC 5 avant 7 (intersection & ordre)
// TODO etudiant : completer le pattern ci-dessous.
// Indice : croisez la contrainte de ligne valide avec .*5.*7.* (5 avant 7).
string ligneAvec5Avant7 = "[1-9]{9}";  // TODO etudiant : completer l'intersection
var exoRe = new Resharp.Regex(ligneAvec5Avant7);
Console.WriteLine("Exercice a completer : 5 doit apparaitre avant 7.");
Console.WriteLine($"  '123456789' (5 avant 7) -> valide attendu, obtenu : {(exoRe.Matches("123456789").Length > 0 ? "valide" : "rejet")}");
Console.WriteLine($"  '987654321' (7 avant 5) -> rejet attendu,  obtenu : {(exoRe.Matches("987654321").Length > 0 ? "valide" : "rejet")}");

Exercice a completer : 5 doit apparaitre avant 7.
  '123456789' (5 avant 7) -> valide attendu, obtenu : valide
  '987654321' (7 avant 5) -> rejet attendu,  obtenu : valide

Annexe A — Les théories derrière le & : M2L-str et décomposition monadique

L’exercice 1 (section 5) exprime ” 5 avant 7 ” comme une intersection de regex (& .*5.*7.*). Mais cette même contrainte admet une troisième écriture - ni regex, ni système d’inégalités : une formule de logique monadique du second ordre sur les chaînes (M2L-str). ” Il existe une position du 5 strictement avant une position du 7 ” s’écrit littéralement

\[\exists\, x,\, y.\quad x < y \;\wedge\; P_5(x) \;\wedge\; P_7(y)\]

ou \(P_d(i)\) signifie ” la case \(i\) porte le chiffre \(d\) “. C’est mot pour mot l’exemple introductif des slides de référence de Margus Veanes (Dagstuhl 17142, 2017) : exists x,y. x<y && a(x) && b(y).

L’intérêt de ce registre : un compilateur de logique (D’Antoni & Veanes, POPL’17 ; outil s-M2L-str) transforme automatiquement une telle formule en automate symbolique (SFA). On décrit la propriété ; la machine fabrique le reconnaisseur - on n’écrit ni l’automate, ni la regex. Trois registres pour une seule et même contrainte :

Registre	Ce qu’on écrit	Qui fabrique le reconnaisseur / la solution
Regex symbolique (RE#, ce notebook)	lignevalide & .*5.*7.*	le moteur de dérivées
Logique M2L-str (Veanes & D’Antoni)	exists x,y. x<y && P_5(x) && P_7(y)	le compilateur logique vers SFA
Contraintes (Z3, section 6)	Distinct + appartenances	le solveur SMT

Le même &, vu d’en haut. Les trois registres partagent l’algèbre de Boole des langages réguliers (cf notebook 10, section 3). La conjonction logique && de M2L-str, l’intersection & de RE# et le re.inter SMT-LIB sont la même opération dans trois notations. Mais la forme sous laquelle on émet cette conjonction décide si Z3 atterrit le 9x9 (section 6b) - une question que la théorie de Veanes nomme décomposition monadique, et que l’ordre x < y de cet exercice illustre justement par la négative (cf section 6b).

6. Le résolveur - Z3 produit le témoin

RE# sait vérifier ; il ne sait pas produire. Pour résoudre un puzzle Sudoku, il faut un résolveur. C’est le rôle de Z3, et c’est le barreau 2 de 2020 - mais cette fois sans le cap de 21 caractères, parce qu’on appelle Z3 directement (sans passer par le chemin SFAz3 de AutomataDotNet qui était muré).

L’idée : encoder les contraintes Ligne & Colonne & Bloc non plus comme un regex symbolique, mais comme des assertions SMT sur 81 variables entières, puis demander à Z3 un modèle = la grille solution.

Note technique : comme pour RE#, on charge Z3 via référence DLL à chemin relatif + un NativeLibrary.SetDllImportResolver pour la librairie native libz3.dll (le #r "nuget:" se bloquerait sous papermill). Les binaires Z3 et le fork Automata (section 6b) vivent dans le .deploy de leurs submodules respectifs (SymbolicAI/SMT/Z3.Linq et .../Automata, série Z3) - à initialiser via git submodule update --init. Plus aucun chemin utilisateur code en dur.

// Z3 chargee par chemin RELATIF au depot (.deploy) + resolver natif (libz3.dll), pas de #r "nuget:" sous papermill.
// Plus aucun chemin utilisateur code en dur. Les binaires Z3 proviennent du .deploy du submodule Z3.Linq (serie Z3).
#r "../SymbolicAI/SMT/Z3.Linq/.deploy/Microsoft.Z3.dll"
using Microsoft.Z3;
using System.IO;
using System.Runtime.InteropServices;

// Z3 est une librairie native (libz3.dll) ; on la résout a cote du Microsoft.Z3.dll charge (même dossier .deploy).
NativeLibrary.SetDllImportResolver(typeof(Context).Assembly, (name, assembly, path) => {
    if (name == "libz3") {
        string asmDir = Path.GetDirectoryName(typeof(Context).Assembly.Location);
        string[] cands = {
            Path.Combine(asmDir ?? ".", "libz3.dll"),
            Path.GetFullPath("../SymbolicAI/SMT/Z3.Linq/.deploy/libz3.dll"),
            "../SymbolicAI/SMT/Z3.Linq/.deploy/libz3.dll"
        };
        foreach (var c in cands) if (File.Exists(c) && NativeLibrary.TryLoad(c, out IntPtr h)) return h;
    }
    return IntPtr.Zero;
});
var ctx = new Context();
Console.WriteLine($"Z3 charge (native libz3 resolue, .deploy submodule Z3.Linq). Version {Microsoft.Z3.Version.FullVersion}.");

Z3 charge (native libz3 resolue, .deploy submodule Z3.Linq). Version Z3 4.12.2.0.

using Microsoft.Z3;
using System.Text;

// Resolution du Sudoku par Z3 : 81 entiers + Distinct sur lignes/colonnes/blocs.
// C'est le VRAI resolveur de production (le témoin = la grille solution).
static int[,] ResoudreSudokuZ3(Context ctx, int[,] puzzle, out long ms)
{
    var sw = System.Diagnostics.Stopwatch.StartNew();
    var cells = new IntExpr[9, 9];
    var solver = ctx.MkSolver();
    for (int r = 0; r < 9; r++)
        for (int c = 0; c < 9; c++)
        {
            cells[r, c] = (IntExpr)ctx.MkConst($"c_{r}_{c}", ctx.IntSort);
            solver.Assert(ctx.MkAnd(ctx.MkLe(ctx.MkInt(1), cells[r, c]),
                                    ctx.MkLe(cells[r, c], ctx.MkInt(9))));
            if (puzzle[r, c] != 0)
                solver.Assert(ctx.MkEq(cells[r, c], ctx.MkInt(puzzle[r, c])));
        }
    // Lignes et colonnes : tous distincts
    for (int i = 0; i < 9; i++)
    {
        var ligne = new IntExpr[9];
        var colonne = new IntExpr[9];
        for (int j = 0; j < 9; j++) { ligne[j] = cells[i, j]; colonne[j] = cells[j, i]; }
        solver.Assert(ctx.MkDistinct(ligne));
        solver.Assert(ctx.MkDistinct(colonne));
    }
    // Blocs 3x3 : tous distincts
    for (int br = 0; br < 3; br++)
        for (int bc = 0; bc < 3; bc++)
        {
            var bloc = new IntExpr[9];
            int k = 0;
            for (int r = 0; r < 3; r++)
                for (int c = 0; c < 3; c++)
                    bloc[k++] = cells[br * 3 + r, bc * 3 + c];
            solver.Assert(ctx.MkDistinct(bloc));
        }

    var res = new int[9, 9];
    if (solver.Check() == Status.SATISFIABLE)
    {
        var m = solver.Model;
        for (int r = 0; r < 9; r++)
            for (int c = 0; c < 9; c++)
                res[r, c] = ((IntNum)m.Eval(cells[r, c], true)).Int;
    }
    sw.Stop();
    ms = sw.ElapsedMilliseconds;
    return res;
}

// Rendu de la grille en UNE seule chaîne (lignes uniformes, separateurs alignes) pour
// eviter les sauts de ligne fragmentes qui s'affichent mal sous Jupyter / GitHub.
static string RendreGrille(int[,] g)
{
    var sb = new StringBuilder();
    string sep = "------+-------+------";
    for (int r = 0; r < 9; r++)
    {
        for (int c = 0; c < 9; c++)
        {
            sb.Append(g[r, c]);
            if (c == 2 || c == 5) sb.Append(" | ");
            else if (c < 8)       sb.Append(' ');
        }
        sb.Append('\n');
        if (r == 2 || r == 5) sb.Append(sep).Append('\n');
    }
    return sb.ToString();
}

// Puzzle classique (exemple Wikipedia). 0 = case vide.
int[,] 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}
};

long msSolve;
var solution = ResoudreSudokuZ3(ctx, puzzle, out msSolve);
Console.WriteLine($"Z3 a produit un temoin (grille solution) en {msSolve} ms :\n");
Console.Write(RendreGrille(solution));

Z3 a produit un temoin (grille solution) en 44 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

Interprétation : Z3 = production du témoin (le travail dur)

Z3 a produit la grille solution - le témoin - en quelques dizaines de millisecondes. C’est le barreau 2 de 2020, mais sans le cap de 21 caractères : on appelle Z3 directement, pas via le chemin SFAz3 qui était tronqué. C’est ce résolveur qui entre dans le benchmark Sudoku multi-paradigmes (aux côtés d’Infer.NET, du PSO, du réseau de neurones) : il résout réellement le dataset.

C’est aussi le “cop-out” de l’ancienne version de ce notebook qu’on tue ici : non, “utiliser Z3 directement” n’est pas une dégression honteuse par rapport aux automates - c’est le complément indispensable du vérificateur RE#. Solving (Z3) et matching (RE#) sont les deux faces de la série.

6b. Les deux murs tombent - et la dernière marche, c’est la forme d’émission

Le barreau 2 (2020) butait sur deux murs, tous deux liés à la matérialisation d’un automate : l’explosion du produit de DFA (mur 1) ET le cap du témoin à ~21 caractères (mur 2, issue #6). Le fork Automata (modernisation net8.0, MyIntelligenceAgency) change de moteur : son RegexToSMTConverter compile la syntaxe de surface & / ~ vers la théorie des chaînes SMT-LIB 2.6 (re.inter, re.comp, re.range, re.loop, str.to_re) - le dialecte que Z3 consomme directement.

Conséquence : Z3 raisonne symboliquement sur les chaînes, sans jamais construire le produit d’automates. Le mur 1 (explosion DFA) n’est donc pas “levé” - il n’est plus rencontre. Et le mur 2 (cap) disparaît : un témoin de 30 caractères pour [a-z]{30} sort sans problème.

Restait une dernière marche, le 9x9. Et là, ce n’est ni le substrat ni le moteur qui décide, mais la forme d’émission du même & d’appartenances :

Échelle	Forme d’émission du tous-distincts	Témoin via la théorie des chaînes Z3
A & ~B général (mot de passe, entrée de test)	re.inter / re.comp	rapide (~100 ms, cf notebook 10)
Grille 4x4 (Shidoku)	appartenance fondue en re.inter	atterrit (~1,7 s, cellule plus bas)
1 ligne 9x9 (9 cases)	appartenance fondue en re.inter (10-way)	atterrit mais lent (~12,5 s)
Grille 9x9	appartenance fondue en re.inter (27 groupes qui se chevauchent)	unknown (au-delà d’une minute - le produit d’automates sature)
Grille 9x9	appartenance éclatée : chaque .*d.* en str.contains natif	atterrit (~53 s en .NET, ~12 s z3-py - section 6c)
Grille 9x9	inégalités 2 à 2 (= Distinct développé)	atterrit (~0,8 s, cellule suivante)

La grille 9x9 n’est bloquée ni par un mur d’automate, ni par le substrat chaîne, ni même par l’appartenance régulière : elle l’est seulement quand on fond les 27 intersections k-way en un produit re.inter que Z3 doit matérialiser au solve. Éclate ce même & d’appartenances en la primitive native str.contains (un par chiffre - section 6c) et la grille atterrit, sans une seule inégalité. Les inégalités 2 à 2 (ci-dessous) atterrissent plus vite encore, mais elles quittent le regex ; la forme la plus pure - le regex qui se suffit à lui-même - est str.contains. Le critère décisif n’est donc pas “appartenance vs inégalité” ni “1D vs 2D” : c’est produit d’automates fondu vs primitive native éclatée.

// Le fork Automata compile la MEME intersection 10-way que RE# vérifie (section 5) vers la
// THEORIE DES CHAINES de Z3 (re.inter / re.comp / re.range), PAS vers un produit d'automates.
// On boucle la chaîne SMT -> Z3 -> témoin, puis on CROISE les moteurs : le témoin doit être
// VALIDE par le verificateur RE# `ligneValide` (section 5).
#r "../SymbolicAI/SMT/Automata/.deploy/System.CodeDom.dll"
#r "../SymbolicAI/SMT/Automata/.deploy/Microsoft.Automata.dll"
using System;
using System.Linq;
using System.Diagnostics;
using Microsoft.Automata;
using Microsoft.Z3;

var conv = new RegexToSMTConverter(BitWidth.BV7);
string ligneSurface = "^[1-9]{9}$&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*";
Console.WriteLine("NOTRE regex - l'intersection 10-way en syntaxe de surface & (celui qu'on veut voir) :");
Console.WriteLine("  " + ligneSurface);
Console.WriteLine();
string smtLigne = conv.ConvertRegex(ligneSurface);   // dialecte SMT-LIB 2.6 (théorie des chaînes)
Console.WriteLine($"Le fork emet du SMT-LIB 2.6 ({smtLigne.Length} caracteres). Tete :");
Console.WriteLine("  " + smtLigne.Substring(0, Math.Min(150, smtLigne.Length)) + " ...");
Console.WriteLine();

// On résout ce terme regex via Z3 (ctx defini section 6) : (str.in_re w <terme>).
string script = "(declare-const w String)\n(assert (str.in_re w " + smtLigne + "))\n(check-sat)";
var sw = Stopwatch.StartNew();
var asserts = ctx.ParseSMTLIB2String(script);
var solver = ctx.MkSolver();
solver.Assert(asserts);
var status = solver.Check();
string temoinLigne = null;
if (status == Status.SATISFIABLE)
{
    var w = (SeqExpr)ctx.MkConst("w", ctx.StringSort);
    temoinLigne = solver.Model.Eval(w, true).ToString().Trim('"');
}
sw.Stop();

bool permutation = temoinLigne != null && temoinLigne.Length == 9 &&
                   Enumerable.Range(1, 9).All(d => temoinLigne.Contains((char)('0' + d)));
bool valideParREsharp = temoinLigne != null && ligneValide.Matches(temoinLigne).Length > 0;

Console.WriteLine($"Temoin Z3 (1 ligne, theorie des chaines) : {temoinLigne}   [{status}]");
Console.WriteLine($"  permutation de 1..9     : {permutation}");
Console.WriteLine($"  valide selon RE#        : {valideParREsharp}  (validation croisee inter-moteurs)");
Console.WriteLine($"  temps generation temoin : {sw.Elapsed.TotalMilliseconds:F0} ms");
Console.WriteLine();
Console.WriteLine("Mur 2 (cap ~21 char) : disparu - temoin complet de 9 caracteres.");
Console.WriteLine("Mur 1 (explosion DFA) : non rencontre - aucun produit d'automates n'est construit.");
Console.WriteLine("Cout dans le solveur de chaines : ~10 s sur cette intersection 10-way (1D),");
Console.WriteLine("vs ~100 ms pour un 'A & ~B' general (NB06). Et une GRILLE entiere (2D) ? -> cellule suivante.");

NOTRE regex - l'intersection 10-way en syntaxe de surface & (celui qu'on veut voir) :
  ^[1-9]{9}$&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*

Le fork emet du SMT-LIB 2.6 (1765 caracteres). Tete :
  (re.inter (re.++ (str.to_re "")(re.++ ((_ re.loop 9 9) (re.range "1" "9")) (str.to_re "")))(re.inter (re.++ (re.* (re.union (re.range "\u{0}" "\u{9}") ...

Temoin Z3 (1 ligne, theorie des chaines) : 129745836   [SATISFIABLE]
  permutation de 1..9     : True
  valide selon RE#        : True  (validation croisee inter-moteurs)
  temps generation temoin : 12131 ms

Mur 2 (cap ~21 char) : disparu - temoin complet de 9 caracteres.
Mur 1 (explosion DFA) : non rencontre - aucun produit d'automates n'est construit.
Cout dans le solveur de chaines : ~10 s sur cette intersection 10-way (1D),
vs ~100 ms pour un 'A & ~B' general (NB06). Et une GRILLE entiere (2D) ? -> cellule suivante.

La boucle est bouclée : notre regex résout une grille COMPLETE (4x4)

Une ligne, c’est 1D. Une grille est 2D : chaque case appartient simultanément à une ligne, une colonne ET un bloc. Donnons à Z3 les 16 cases d’un Shidoku (Sudoku 4x4) comme 16 chaînes d’un caractère, et imposons que chaque ligne, chaque colonne et chaque bloc satisfasse la même intersection - notre regex ^[1-4]{4}$ & .*1.* & .*2.* & .*3.* & .*4.*. Aucun produit d’automates, aucun cap de témoin : le fork compile notre regex en théorie des chaînes, et Z3 produit la grille entière.

C’est l’aboutissement concret de l’échelle : un beau regex d’intersection en entrée, une grille résolue en sortie. La voie symbolique atterrit.

// === La boucle bouclee : NOTRE regex résout une grille COMPLETE (4x4 Shidoku) via la théorie des chaînes ===
// Chaque ligne, colonne ET bloc doit satisfaire la MEME intersection (notre regex). Z3 produit la grille.
using System.Text;
using System.Linq;

var conv4 = new RegexToSMTConverter(BitWidth.BV7);
string regle4 = "^[1-4]{4}$&.*1.*&.*2.*&.*3.*&.*4.*";   // NOTRE beau regex : permutation de 1..4
Console.WriteLine("Notre regex (intersection 4-way, syntaxe de surface &) - celui qu'on veut voir :");
Console.WriteLine("  " + regle4 + "\n");
string re4 = conv4.ConvertRegex(regle4);                 // -> terme re.inter SMT-LIB 2.6 (reutilise 12x)
Console.WriteLine($"Compile en theorie des chaines SMT-LIB 2.6 ({re4.Length} car.), tete :");
Console.WriteLine("  " + re4.Substring(0, Math.Min(96, re4.Length)) + " ...\n");

var sb = new StringBuilder();
for (int r = 0; r < 4; r++) for (int c = 0; c < 4; c++) sb.AppendLine($"(declare-const s_{r}_{c} String)");
for (int r = 0; r < 4; r++) for (int c = 0; c < 4; c++) sb.AppendLine($"(assert (= (str.len s_{r}_{c}) 1))");
// 12 contraintes = la MEME intersection (notre regex) sur lignes, colonnes, blocs 2x2.
for (int r = 0; r < 4; r++) { var g = string.Join(" ", Enumerable.Range(0, 4).Select(c => $"s_{r}_{c}")); sb.AppendLine($"(assert (str.in_re (str.++ {g}) {re4}))"); }
for (int c = 0; c < 4; c++) { var g = string.Join(" ", Enumerable.Range(0, 4).Select(r => $"s_{r}_{c}")); sb.AppendLine($"(assert (str.in_re (str.++ {g}) {re4}))"); }
for (int br = 0; br < 2; br++) for (int bc = 0; bc < 2; bc++) { var g = string.Join(" ", from dr in Enumerable.Range(0, 2) from dc in Enumerable.Range(0, 2) select $"s_{br*2+dr}_{bc*2+dc}"); sb.AppendLine($"(assert (str.in_re (str.++ {g}) {re4}))"); }
// Le puzzle de depart (quelques indices)
sb.AppendLine($@"(assert (= s_0_0 ""1""))");
sb.AppendLine($@"(assert (= s_1_2 ""1""))");
sb.AppendLine($@"(assert (= s_3_3 ""2""))");
sb.AppendLine("(check-sat)");

var sw4 = Stopwatch.StartNew();
var asserts4 = ctx.ParseSMTLIB2String(sb.ToString());
var solver4 = ctx.MkSolver();
solver4.Assert(asserts4);
var st4 = solver4.Check();
sw4.Stop();

Console.WriteLine($"Z3 (12 contraintes = NOTRE regex, theorie des chaines) : {st4} en {sw4.Elapsed.TotalMilliseconds:F0} ms\n");
if (st4 == Status.SATISFIABLE) {
    var m = solver4.Model;
    Console.WriteLine("Grille 4x4 produite par NOTRE regex -> theorie des chaines Z3 :");
    for (int r = 0; r < 4; r++) {
        var line = new StringBuilder("    ");
        for (int c = 0; c < 4; c++) {
            var v = (SeqExpr)ctx.MkConst($"s_{r}_{c}", ctx.StringSort);
            line.Append(m.Eval(v, true).ToString().Trim('"'));
            if (c == 1) line.Append(" | "); else if (c < 3) line.Append(' ');
        }
        Console.WriteLine(line.ToString());
        if (r == 1) Console.WriteLine("    ----+----");
    }
    Console.WriteLine("\nLa boucle est bouclee : un beau regex d'intersection en entree, une grille resolue en sortie.");
    Console.WriteLine("La voie symbolique ATTERRIT. (Le 9x9 demandera un autre encodage : cellule suivante.)");
} else {
    Console.WriteLine($"Statut inattendu : {st4}");
}

Notre regex (intersection 4-way, syntaxe de surface &) - celui qu'on veut voir :
  ^[1-4]{4}$&.*1.*&.*2.*&.*3.*&.*4.*

Compile en theorie des chaines SMT-LIB 2.6 (830 car.), tete :
  (re.inter (re.++ (str.to_re "")(re.++ ((_ re.loop 4 4) (re.range "1" "4")) (str.to_re "")))(re.i ...

Z3 (12 contraintes = NOTRE regex, theorie des chaines) : SATISFIABLE en 1387 ms

Grille 4x4 produite par NOTRE regex -> theorie des chaines Z3 :
    1 3 | 2 4
    2 4 | 1 3
    ----+----
    4 2 | 3 1
    3 1 | 4 2

La boucle est bouclee : un beau regex d'intersection en entree, une grille resolue en sortie.
La voie symbolique ATTERRIT. (Le 9x9 demandera un autre encodage : cellule suivante.)

int groupes = 9 + 9 + 9;                        // 27
int sousContraintesParGroupe = 1 + 9;           // 1 longueur + 9 presences de chiffre
int total = groupes * sousContraintesParGroupe; // 270

Console.WriteLine($"Grille 9x9 (encodage APPARTENANCE) = {groupes} groupes x {sousContraintesParGroupe} = {total} sous-contraintes.");
Console.WriteLine();
Console.WriteLine("Le 4x4 ATTERRIT par NOTRE regex (appartenance a l'intersection). Et le 9x9 par la meme voie ?");
Console.WriteLine("  - une SEULE ligne (intersection 10-way) demande deja ~10 s (mesure plus haut) ;");
Console.WriteLine("  - lignes/colonnes/blocs se CHEVAUCHENT (chaque case appartient a 3 groupes) :");
Console.WriteLine("    a 81 cases, le tous-distincts en APPARTENANCE regex sature -> Z3 'unknown' (> 60 s, section 8).");
Console.WriteLine();
Console.WriteLine("ATTENTION au diagnostic : ce n'est PAS le substrat chaine qui mure (ni une affaire de '1D vs 2D').");
Console.WriteLine("C'est l'ENCODAGE du tous-distincts en appartenance reguliere qui ne passe pas l'echelle.");
Console.WriteLine("On garde les memes 81 chaines d'un caractere, et on ecrit le tous-distincts EN INEGALITES 2 A 2");
Console.WriteLine("  -> la grille 9x9 COMPLETE atterrit en theorie des chaines (cellule suivante).");
Console.WriteLine("En production : Distinct sur 81 entiers (section 6, ~47 ms) - meme idee, sucre syntaxique du 2 a 2.");

Grille 9x9 (encodage APPARTENANCE) = 27 groupes x 10 = 270 sous-contraintes.

Le 4x4 ATTERRIT par NOTRE regex (appartenance a l'intersection). Et le 9x9 par la meme voie ?
  - une SEULE ligne (intersection 10-way) demande deja ~10 s (mesure plus haut) ;
  - lignes/colonnes/blocs se CHEVAUCHENT (chaque case appartient a 3 groupes) :
    a 81 cases, le tous-distincts en APPARTENANCE regex sature -> Z3 'unknown' (> 60 s, section 8).

ATTENTION au diagnostic : ce n'est PAS le substrat chaine qui mure (ni une affaire de '1D vs 2D').
C'est l'ENCODAGE du tous-distincts en appartenance reguliere qui ne passe pas l'echelle.
On garde les memes 81 chaines d'un caractere, et on ecrit le tous-distincts EN INEGALITES 2 A 2
  -> la grille 9x9 COMPLETE atterrit en theorie des chaines (cellule suivante).
En production : Distinct sur 81 entiers (section 6, ~47 ms) - meme idee, sucre syntaxique du 2 a 2.

Une autre voie qui atterrit : le tous-distincts en inégalités 2 à 2 (plus rapide, mais hors regex)

La section 6c a fait atterrir le 9x9 dans le regex (appartenance pure, str.contains). Il existe une autre forme d’émission qui atterrit, plus rapide encore - mais qui, elle, quitte l’appartenance régulière : écrire le tous-distincts en inégalités 2 à 2.

On garde les 81 chaînes d’un caractère (même substrat), mais pour chaque groupe (ligne, colonne, bloc) et chaque paire de cases, on assert s_i != s_j. C’est “écrivable à l’huile de coude” - 972 inégalités générées en boucle - et, côté Z3, ca ne change pas la nature du problème : Distinct n’est lui-même que du sucre syntaxique pour ces inégalités 2 à 2 (intuition de perf confirmée : le coût vient de la combinatoire, pas de la syntaxe).

Résultat : la grille 9x9 complète sort en théorie des chaînes, de l’ordre de la seconde (~0,8 s, mesure ci-dessous, validée) - soit ~60x plus vite que l’appartenance str.contains (~53 s). Le compromis est clair : l’appartenance pure (6c) est la forme la plus fidèle à la vision 2020 (le regex se suffit, 0 inégalité) ; les inégalités sont la forme la plus rapide (mais ce ne sont plus un regex).

Subtilité honnête. Un vrai “2 à 2 en regex pur” ((.).*\1 : “deux fois le même caractère”) utilise une back-référence - donc un langage non régulier, qui ne compile ni vers la théorie re de Z3 ni via le convertisseur &/~. Le 2 à 2 de cette cellule est exprimé comme inégalités SMT ((not (= s_i s_j))), pas comme regex. La voie qui reste dans le regex, c’est l’appartenance .*d.* émise en str.contains (section 6c) ; celle-ci, en inégalités, en sort. Les deux atterrissent ; seule la première honore “le regex se suffit à lui-même”.

// === Le 9x9 COMPLET atterrit en théorie des chaînes : tous-distincts en INEGALITES 2 A 2 (intuition de l'auteur) ===
// Meme substrat que le 4x4 (81 chaînes d'un caractère). On change SEULEMENT l'encodage du tous-distincts :
// non plus une appartenance regex (qui sature -> unknown), mais des inégalités 2 a 2  s_i != s_j  par groupe.
using System.Text;
using System.Linq;
using System.Collections.Generic;

// Grille canonique (30 indices) - '.' = case a deviner
string[] grille9 = {
    "53..7....",
    "6..195...",
    ".98....6.",
    "8...6...3",
    "4..8.3..1",
    "7...2...6",
    ".6....28.",
    "...419..5",
    "....8..79",
};

var sb9 = new StringBuilder();
for (int r = 0; r < 9; r++) for (int c = 0; c < 9; c++) sb9.AppendLine($"(declare-const s_{r}_{c} String)");
// chaque case : un caractère, dans l'alphabet 1..9
for (int r = 0; r < 9; r++) for (int c = 0; c < 9; c++) {
    sb9.AppendLine($"(assert (= (str.len s_{r}_{c}) 1))");
    sb9.AppendLine($"(assert (str.in_re s_{r}_{c} (re.range \"1\" \"9\")))");
}
// les 27 groupes (lignes, colonnes, blocs) ; tous-distincts = inégalités 2 a 2
var groupes9 = new List<List<(int r, int c)>>();
for (int r = 0; r < 9; r++) groupes9.Add(Enumerable.Range(0, 9).Select(c => (r, c)).ToList());
for (int c = 0; c < 9; c++) groupes9.Add(Enumerable.Range(0, 9).Select(r => (r, c)).ToList());
for (int br = 0; br < 3; br++) for (int bc = 0; bc < 3; bc++)
    groupes9.Add((from dr in Enumerable.Range(0, 3) from dc in Enumerable.Range(0, 3) select (br * 3 + dr, bc * 3 + dc)).ToList());
int nbIneg = 0;
foreach (var g in groupes9)
    for (int i = 0; i < g.Count; i++) for (int j = i + 1; j < g.Count; j++) {
        sb9.AppendLine($"(assert (not (= s_{g[i].r}_{g[i].c} s_{g[j].r}_{g[j].c})))");
        nbIneg++;
    }
// les indices du puzzle
int nbIndices = 0;
for (int r = 0; r < 9; r++) for (int c = 0; c < 9; c++) {
    char ch = grille9[r][c];
    if (ch != '.' && ch != '0') { sb9.AppendLine($"(assert (= s_{r}_{c} \"{ch}\"))"); nbIndices++; }
}
sb9.AppendLine("(check-sat)");

Console.WriteLine($"Encodage : 81 chaines d'un caractere + {nbIneg} inegalites 2 a 2 (27 groupes) + {nbIndices} indices.");
Console.WriteLine("Tous-distincts en INEGALITES (s_i != s_j), PAS en appartenance regex.\n");

var sw9 = Stopwatch.StartNew();
var asserts9 = ctx.ParseSMTLIB2String(sb9.ToString());
var solver9 = ctx.MkSolver();
solver9.Assert(asserts9);
var st9 = solver9.Check();
sw9.Stop();

Console.WriteLine($"Z3 (theorie des chaines, tous-distincts 2 a 2) : {st9} en {sw9.Elapsed.TotalMilliseconds:F0} ms\n");
if (st9 == Status.SATISFIABLE) {
    var m = solver9.Model;
    string[,] sol = new string[9, 9];
    for (int r = 0; r < 9; r++) for (int c = 0; c < 9; c++) {
        var v = (SeqExpr)ctx.MkConst($"s_{r}_{c}", ctx.StringSort);
        sol[r, c] = m.Eval(v, true).ToString().Trim('"');
    }
    Console.WriteLine("Grille 9x9 COMPLETE produite par la theorie des chaines Z3 (a partir de NOTRE substrat) :");
    for (int r = 0; r < 9; r++) {
        var line = new StringBuilder("    ");
        for (int c = 0; c < 9; c++) {
            line.Append(sol[r, c]);
            line.Append(c % 3 == 2 && c < 8 ? " | " : " ");
        }
        Console.WriteLine(line.ToString());
        if (r % 3 == 2 && r < 8) Console.WriteLine("    ------+-------+------");
    }
    bool ok = true;
    foreach (var g in groupes9) {
        var vals = g.Select(p => sol[p.r, p.c]).OrderBy(x => x).ToList();
        if (!vals.SequenceEqual(Enumerable.Range(1, 9).Select(d => d.ToString()))) ok = false;
    }
    Console.WriteLine($"\nValidation (27 groupes = permutation de 1..9) : {(ok ? "OK - grille correcte" : "ECHEC")}.");
    Console.WriteLine("Le mur du 9x9 n'etait pas le substrat chaine : c'etait l'encodage du tous-distincts.");
    Console.WriteLine("Meme substrat, encodage 2 a 2 -> la voie symbolique atterrit la GRILLE 9x9 COMPLETE.");
} else {
    Console.WriteLine($"Statut inattendu : {st9}");
}

Encodage : 81 chaines d'un caractere + 972 inegalites 2 a 2 (27 groupes) + 30 indices.
Tous-distincts en INEGALITES (s_i != s_j), PAS en appartenance regex.

Z3 (theorie des chaines, tous-distincts 2 a 2) : SATISFIABLE en 728 ms

Grille 9x9 COMPLETE produite par la theorie des chaines Z3 (a partir de NOTRE substrat) :
    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 

Validation (27 groupes = permutation de 1..9) : OK - grille correcte.
Le mur du 9x9 n'etait pas le substrat chaine : c'etait l'encodage du tous-distincts.
Meme substrat, encodage 2 a 2 -> la voie symbolique atterrit la GRILLE 9x9 COMPLETE.

Interprétation : les deux murs tombent, et la forme d’émission franchit le 9x9

La chaîne moderne débride le témoin : une ligne Sudoku (intersection 10-way) produit désormais un témoin réel, valide par RE# (validation croisée inter-moteurs ci-dessus) - chose impossible en 2020 sous le cap des 21 caractères. Et aucun produit d’automates n’est construit, donc le “trop d’états” de 2020 ne se produit pas. Les deux murs sont derrière nous.

Reste la dernière marche, le 9x9, et c’est la forme d’émission du même & d’appartenances qui la franchit :

Forme d’émission	Reconnaissance	Production de témoin	Grille 9x9
RE# (2025)	temps linéaire	aucun témoin	vérifie seulement
chaînes Z3, appartenance fondue en re.inter	(oui)	non capé, sans produit d’automates	unknown (le produit sature)
chaînes Z3, appartenance éclatée en str.contains	(oui)	grille complète	atterrit (~53 s)
chaînes Z3, tous-distincts en inégalités 2 à 2	(oui)	grille complète	atterrit (~0,8 s)
Z3 Distinct (entiers)	-	grille complète	~38 ms (production)

Murs tombés, forme d’émission décisive. Le payoff général de la génération de témoin A & ~B est démontré dans le notebook 10 - Générer un témoin depuis A & ~B de la série Z3. Le Sudoku, lui, montre la leçon la plus fine : ce n’est ni le moteur ni le substrat, ni même “appartenance vs inégalité” qui décide, mais la forme d’émission du même & d’appartenances - fondu en re.inter (sature au 9x9) vs éclaté en str.contains natif (atterrit). Le regex n’est pas le mauvais outil : bien émis, il atterrit la grille 9x9 complète, sans une seule inégalité.

La théorie derrière la ” forme d’émission ” : la décomposition monadique (Veanes, CAV’14)

Le tableau de la section 6b est un constat empirique : fondue en re.inter, l’appartenance sature ; éclatée en str.contains, elle atterrit. Cette observation porte un nom et possède une théorie chez Veanes : la décomposition monadique (Monadic Décomposition, M. Veanes, N. Bjorner, L. Nachmanson, S. Bereg, CAV 2014).

Une contrainte à plusieurs variables est monadiquement décomposable si elle équivaut à une combinaison booléenne de prédicats à une seule variable (” monadiques “). Quand elle l’est, on peut remplacer un produit (le re.inter qui matérialise l’espace croisé) par une conjonction de tests indépendants - exactement le passage de l’appartenance fondue aux str.contains éclatés par chiffre qui fait atterrir le 9x9, sans jamais construire le produit d’automates.

Le théorème précise quand cet éclatement existe :

Contrainte	Monadiquement décomposable ?	Conséquence pour l’émission
tous-distincts par appartenances (.*d.* par chiffre)	oui	éclatable en str.contains -> atterrit
x + (y mod 2) > 5	oui (combinaison Cartésienne finie)	produit fini, gérable
x < y (ordre entre deux positions)	non - aucune décomposition monadique finie	reste un produit ; sature si émis fondu

De ” j’ai essayé ” à ” j’ai retrouvé le principe “.** Le notebook a découvert en mesurant que l’appartenance éclatée atterrit ; la décomposition monadique en est la raison formelle. Elle éclaire aussi la limite : la contrainte” 5 avant 7 ” de l’exercice 1 repose sur x < y, le prédicat que Veanes donne précisément comme contre-exemple** sans décomposition finie. L’ordre ne s’éclate pas ; le tous-distincts, si. Côté reconnaissance, la même économie d’états est garantie par la finitude des dérivées - le notebook Lean-14, troisième pilier du triptyque #2978.

6c. Le regex qui se suffit à lui-même - et qui atterrit le 9x9 (vision 2020, mesurée)

Les sections 6 / 6b ont séparé le domaine, les indices et le tous-distincts. On revient maintenant à la forme la plus pure de l’idée de départ : un seul regex qui se suffit à lui-même, ou toutes les contraintes - domaine, indices, et tous-distincts - sont portées par l’appartenance à une intersection &, et où Z3 ne fait plus que chercher un témoin. Aucune inégalité, rien hors du regex : le regex est le problème.

On ferme la boucle dans la forme attendue par la série : un solveur qui implémente ISudokuSolver (SudokuGrid Solve(SudokuGrid)), charge un puzzle réel depuis les fichiers partagés Puzzles/, et génère le regex dynamiquement à partir de ce puzzle - le regex qu’on voulait voir affiche.

• chaque case ∈ son fragment (d -> d ; vide -> [1-9]) : domaine + indices ;
• chaque groupe (lignes, colonnes, blocs – 27 au total) : la concaténation de ses 9 cases ∈ la règle d’unicité ^[1-9]{9}$ & .*1.* & ... & .*9.* (= permutation de 1..9) : tous-distincts EN REGEX, zéro inégalité.

Note d’implémentation. Le notebook reste autonome - il ne charge que des binaires .deploy, jamais un autre notebook, ce qui le rend rejouable headless sous papermill. On reproduit donc ici, en version compacte, l’interface ISudokuSolver et la classe SudokuGrid de la série (mêmes signatures) : un solveur écrit ici se branche tel quel dans le projet Sudoku.

La clé - et c’est le coeur du notebook. Le tous-distincts d’un groupe est la conjonction d’appartenances .*1.* & .*2.* & ... & .*9.*. Or chaque conjonct .*d.* a une primitive native dans la théorie des chaînes : (str.contains g "d"). C’est exactement .*d.*, mais émis comme prédicat propre au lieu d’être fondu dans un produit d’automates :

• fondu : (str.in_re g (re.inter (.*1.*) ... (.*9.*))) -> Z3 matérialise les produits d’automates au solve, sur 27 groupes qui se chevauchent -> unknown (au-delà d’une minute) ;
• éclaté : (str.contains g "d") par chiffre -> primitive bien propagée -> SATISFIABLE (~53 s en .NET, ~12 s en z3-py).

C’est le même & d’appartenances, zéro inégalité : seule la forme d’émission change. C’est cela, l’élément de syntaxe entrevu en 2020 - et c’est ce qui fait atterrir la grille 9x9 complète depuis le seul regex. Sur la grille 4x4 (Shidoku), l’appartenance atterrit même fondue en re.inter (~1,7 s, section 6b) ; au 9x9, il faut l’éclater en str.contains. La grille produite ci-dessous est réelle, validée (27 groupes = permutation de 1..9), et sort de la seule appartenance regex -> théorie des chaînes. Le regex qui se suffit à lui-même n’est donc pas borné au 4x4 : il atterrit le 9x9. (Les inégalités 2 à 2 - section suivante - sont ~60x plus rapides, mais elles quittent le regex ; ici, le regex se suffit.)

using System;
using System.IO;
using System.Linq;
using System.Text;

// La serie Sudoku fournit une interface (ISudokuSolver) et une grille (SudokuGrid). On les reproduit
// ici en version compacte (memes signatures) pour garder CE notebook autonome : il ne charge que des
// binaires .deploy, jamais un autre notebook - c'est ce qui le rend rejouable headless sous papermill.
public class SudokuGrid
{
    public int[,] Cells { get; set; } = new int[9, 9];
    public SudokuGrid Clone() { var g = new SudokuGrid(); Array.Copy(Cells, g.Cells, Cells.Length); return g; }

    // Parse une grille au format "81 caractères" (1-9 ; '.', '0' ou espace = case vide).
    public static SudokuGrid ReadSudoku(string s)
    {
        var jetons = s.Where(ch => char.IsDigit(ch) || ch == '.').ToArray();
        var g = new SudokuGrid();
        for (int i = 0; i < 81 && i < jetons.Length; i++)
            g.Cells[i / 9, i % 9] = (jetons[i] == '.' || jetons[i] == '0') ? 0 : jetons[i] - '0';
        return g;
    }

    public override string ToString()
    {
        var sb = new StringBuilder();
        for (int r = 0; r < 9; r++)
        {
            if (r % 3 == 0) sb.AppendLine("+-------+-------+-------+");
            var line = new StringBuilder("| ");
            for (int c = 0; c < 9; c++)
            {
                line.Append(Cells[r, c] == 0 ? "." : Cells[r, c].ToString());
                line.Append(c % 3 == 2 ? " | " : " ");
            }
            sb.AppendLine(line.ToString());
        }
        sb.AppendLine("+-------+-------+-------+");
        return sb.ToString();
    }
}

public interface ISudokuSolver
{
    SudokuGrid Solve(SudokuGrid s);
}

// Chargement d'un PUZZLE REEL depuis les fichiers partages de la serie (dossier Puzzles/).
string DossierPuzzles()
{
    foreach (var cand in new[] { "Puzzles", "MyIA.AI.Notebooks/Sudoku/Puzzles", "../Sudoku/Puzzles" })
        if (Directory.Exists(cand)) return cand;
    throw new DirectoryNotFoundException("Dossier Puzzles/ introuvable");
}
string ligneEasy = File.ReadLines(Path.Combine(DossierPuzzles(), "Sudoku_Easy51.txt")).First();
var puzzlePartage = SudokuGrid.ReadSudoku(ligneEasy);
Console.WriteLine("Infra de la serie reproduite (ISudokuSolver / SudokuGrid) ; puzzle reel charge depuis Puzzles/Sudoku_Easy51.txt :");
Console.WriteLine(puzzlePartage.ToString());

Infra de la serie reproduite (ISudokuSolver / SudokuGrid) ; puzzle reel charge depuis Puzzles/Sudoku_Easy51.txt :
+-------+-------+-------+
| 9 . 2 | . . 5 | 4 . 3 | 
| 1 . . | . 6 3 | . 2 5 | 
| 5 . 8 | 4 . 7 | . 6 . | 
+-------+-------+-------+
| . 2 6 | 3 . 9 | . . 1 | 
| . 5 7 | . 1 . | 2 9 . | 
| . 9 . | 6 7 . | 5 3 . | 
+-------+-------+-------+
| 2 4 . | 5 3 . | 6 . . | 
| 7 . 5 | 2 . . | 3 . 4 | 
| . 8 . | . 4 1 | 9 5 . | 
+-------+-------+-------+

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

// VISION 2020 : un REGEX QUI SE SUFFIT A LUI-MEME, et qui ATTERRIT le 9x9.
// Toutes les contraintes - domaine, indices, ET tous-distincts - sont portees par l'APPARTENANCE a un
// regex (intersection &), zero inégalité. Le tous-distincts d'un groupe = la conjonction d'appartenances
//   .*1.* & .*2.* & ... & .*9.*   (= "contient chaque chiffre 1..9" ; sur 9 cases, c'est une permutation).
//
// LA CLEF (l'element de syntaxe vise en 2020). Chaque conjonct d'appartenance ".*d.*" a une primitive
// NATIVE dans la théorie des chaînes de Z3 : (str.contains g "d"). C'est EXACTEMENT ".*d.*", mais emis
// comme predicat propre plutot que fondu dans un produit d'automates (re.inter / str.in_re) :
//   - fondu  : (str.in_re g (re.inter (.*1.*) ... (.*9.*)))  -> Z3 construit les produits au solve -> unknown (>60 s) ;
//   - eclate : (str.contains g "d") par chiffre              -> primitive bien propagee            -> SAT ~12 s.
// Le regex reste integralement le problème (0 inégalité) ; seule la FORME d'emission du MEME & d'appartenances
// change. C'est cela qui fait atterrir le 9x9 en théorie des chaînes - sans jamais sortir du regex.
public class RegexAutoSuffisantSolver : ISudokuSolver
{
    private readonly Context _ctx;
    public string[] RegexParLigne { get; private set; }   // le regex auto-suffisant, ligne par ligne (masque & regle)
    public string RegleUnicite   { get; private set; }
    public long   DernierTempsMs { get; private set; }
    public string Statut         { get; private set; }
    public string SmtConjonctFondu { get; private set; }  // forme SMT "fondue" d'un conjonct .*d.* (pour la pedagogie)

    public RegexAutoSuffisantSolver(Context ctx) { _ctx = ctx; }
    private static string Frag(int v) => v == 0 ? "[1-9]" : v.ToString();
    private const string Unicite = "&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*";

    public SudokuGrid Solve(SudokuGrid s)
    {
        var conv = new RegexToSMTConverter(BitWidth.BV7);
        RegleUnicite = "^[1-9]{9}$" + Unicite;
        // Le regex auto-suffisant affiche, par ligne : le MASQUE du puzzle, INTERSECTE & la regle d'unicite.
        RegexParLigne = Enumerable.Range(0, 9).Select(r =>
            string.Concat(Enumerable.Range(0, 9).Select(c => Frag(s.Cells[r, c]))) + Unicite).ToArray();
        // Forme SMT "fondue" d'un SEUL conjonct .*1.* via le convertisseur du fork (illustration du mur 9x9).
        SmtConjonctFondu = conv.ConvertRegex(".*1.*");

        var sb = new StringBuilder();
        for (int r = 0; r < 9; r++) for (int c = 0; c < 9; c++) sb.AppendLine($"(declare-const s_{r}_{c} String)");
        // (1) domaine + indices : chaque case appartient a son fragment de regex (genere DU puzzle).
        //     "[1-9]" force déjà len=1 + alphabet ; "d" force l'indice. Tout est appartenance regex.
        for (int r = 0; r < 9; r++) for (int c = 0; c < 9; c++)
            sb.AppendLine($"(assert (str.in_re s_{r}_{c} {conv.ConvertRegex(Frag(s.Cells[r, c]))}))");
        // (2) tous-distincts EN REGEX : pour chaque groupe (27) et chaque chiffre d, la concatenation du
        //     groupe satisfait .*d.* -- emis comme la primitive native (str.contains g "d"). 0 inégalité.
        var groupes = new List<(int r, int c)[]>();
        for (int r = 0; r < 9; r++) groupes.Add(Enumerable.Range(0, 9).Select(c => (r, c)).ToArray());
        for (int c = 0; c < 9; c++) groupes.Add(Enumerable.Range(0, 9).Select(r => (r, c)).ToArray());
        for (int br = 0; br < 3; br++) for (int bc = 0; bc < 3; bc++)
            groupes.Add((from dr in Enumerable.Range(0, 3) from dc in Enumerable.Range(0, 3)
                         select (br * 3 + dr, bc * 3 + dc)).ToArray());
        foreach (var g in groupes)
        {
            string cat = $"(str.++ {string.Join(" ", g.Select(p => $"s_{p.r}_{p.c}"))})";
            for (int d = 1; d <= 9; d++)
                sb.AppendLine($"(assert (str.contains {cat} \"{d}\"))");
        }
        sb.AppendLine("(check-sat)");

        var p = _ctx.MkParams(); p.Add("timeout", 120000u);     // garde-fou large (le solve attendu ~12 s)
        var solver = _ctx.MkSolver(); solver.Parameters = p;
        var sw = Stopwatch.StartNew();
        solver.Assert(_ctx.ParseSMTLIB2String(sb.ToString()));
        var status = solver.Check();
        sw.Stop();
        DernierTempsMs = sw.ElapsedMilliseconds; Statut = status.ToString();

        var res = s.Clone();
        if (status == Status.SATISFIABLE)
        {
            var m = solver.Model;
            for (int r = 0; r < 9; r++) for (int c = 0; c < 9; c++)
            {
                var v = (SeqExpr)_ctx.MkConst($"s_{r}_{c}", _ctx.StringSort);
                res.Cells[r, c] = int.Parse(m.Eval(v, true).ToString().Trim('"'));
            }
        }
        return res;
    }
}

// --- Demo : le regex AUTO-SUFFISANT, genere du puzzle REEL, resolu par Z3 en APPARTENANCE PURE ---
var solveurAuto = new RegexAutoSuffisantSolver(ctx);
var grilleAuto  = solveurAuto.Solve(puzzlePartage);

Console.WriteLine("Le REGEX QUI SE SUFFIT A LUI-MEME, genere du puzzle (masque des indices INTERSECTE & la regle d'unicite) :");
foreach (var l in solveurAuto.RegexParLigne) Console.WriteLine("  " + l);
Console.WriteLine();
Console.WriteLine("La meme regle d'unicite gouverne CHAQUE ligne, colonne et bloc (permutation de 1..9) :");
Console.WriteLine("  " + solveurAuto.RegleUnicite);
Console.WriteLine();
Console.WriteLine("LA CLEF : chaque conjonct d'appartenance .*d.* est une primitive native de la theorie des chaines.");
Console.WriteLine("  .*1.* FONDU en automate  : (str.in_re g " + solveurAuto.SmtConjonctFondu + ")  -> sature (unknown >60 s)");
Console.WriteLine("  .*1.* en PRIMITIVE native: (str.contains g \"1\")  [idem pour 2..9]              -> propage (SAT ~12 s)");
Console.WriteLine("  Meme & d'appartenances, 0 inegalite : seule la forme d'emission change.");
Console.WriteLine();
Console.WriteLine($"Z3, APPARTENANCE PURE (0 inegalite, le regex se suffit) : {solveurAuto.Statut} en {solveurAuto.DernierTempsMs} ms");
if (solveurAuto.Statut == "SATISFIABLE")
{
    Console.WriteLine("La grille 9x9 sort de la SEULE appartenance regex -> theorie des chaines :");
    Console.WriteLine(grilleAuto.ToString());
    bool Ok(IEnumerable<int> v) => v.OrderBy(x => x).SequenceEqual(Enumerable.Range(1, 9));
    bool valide = Enumerable.Range(0, 9).All(i =>
            Ok(Enumerable.Range(0, 9).Select(j => grilleAuto.Cells[i, j])) &&
            Ok(Enumerable.Range(0, 9).Select(j => grilleAuto.Cells[j, i])))
        && (from br in Enumerable.Range(0, 3) from bc in Enumerable.Range(0, 3)
            select Ok(from dr in Enumerable.Range(0, 3) from dc in Enumerable.Range(0, 3)
                      select grilleAuto.Cells[br * 3 + dr, bc * 3 + dc])).All(x => x);
    Console.WriteLine($"Validation (27 groupes = permutation de 1..9) : {(valide ? "OK - grille correcte" : "ECHEC")}.");
    Console.WriteLine("Vision 2020 ATTEINTE : le regex se suffit a lui-meme - puzzle -> regex -> theorie des chaines -> grille 9x9.");
}
else
{
    Console.WriteLine($"Z3 ne tranche pas (statut {solveurAuto.Statut}) - inattendu pour str.contains, a investiguer.");
}

Le REGEX QUI SE SUFFIT A LUI-MEME, genere du puzzle (masque des indices INTERSECTE & la regle d'unicite) :
  9[1-9]2[1-9][1-9]54[1-9]3&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*
  1[1-9][1-9][1-9]63[1-9]25&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*
  5[1-9]84[1-9]7[1-9]6[1-9]&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*
  [1-9]263[1-9]9[1-9][1-9]1&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*
  [1-9]57[1-9]1[1-9]29[1-9]&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*
  [1-9]9[1-9]67[1-9]53[1-9]&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*
  24[1-9]53[1-9]6[1-9][1-9]&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*
  7[1-9]52[1-9][1-9]3[1-9]4&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*
  [1-9]8[1-9][1-9]4195[1-9]&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*

La meme regle d'unicite gouverne CHAQUE ligne, colonne et bloc (permutation de 1..9) :
  ^[1-9]{9}$&.*1.*&.*2.*&.*3.*&.*4.*&.*5.*&.*6.*&.*7.*&.*8.*&.*9.*

LA CLEF : chaque conjonct d'appartenance .*d.* est une primitive native de la theorie des chaines.
  .*1.* FONDU en automate  : (str.in_re g (re.++ (re.* (re.union (re.range "\u{0}" "\u{9}") (re.range "\u{b}" "\u{7f}")))(re.++ (str.to_re "1") (re.* (re.union (re.range "\u{0}" "\u{9}") (re.range "\u{b}" "\u{7f}"))))))  -> sature (unknown >60 s)
  .*1.* en PRIMITIVE native: (str.contains g "1")  [idem pour 2..9]              -> propage (SAT ~12 s)
  Meme & d'appartenances, 0 inegalite : seule la forme d'emission change.

Z3, APPARTENANCE PURE (0 inegalite, le regex se suffit) : SATISFIABLE en 32254 ms
La grille 9x9 sort de la SEULE appartenance regex -> theorie des chaines :
+-------+-------+-------+
| 9 6 2 | 1 8 5 | 4 7 3 | 
| 1 7 4 | 9 6 3 | 8 2 5 | 
| 5 3 8 | 4 2 7 | 1 6 9 | 
+-------+-------+-------+
| 8 2 6 | 3 5 9 | 7 4 1 | 
| 3 5 7 | 8 1 4 | 2 9 6 | 
| 4 9 1 | 6 7 2 | 5 3 8 | 
+-------+-------+-------+
| 2 4 9 | 5 3 8 | 6 1 7 | 
| 7 1 5 | 2 9 6 | 3 8 4 | 
| 6 8 3 | 7 4 1 | 9 5 2 | 
+-------+-------+-------+

Validation (27 groupes = permutation de 1..9) : OK - grille correcte.
Vision 2020 ATTEINTE : le regex se suffit a lui-meme - puzzle -> regex -> theorie des chaines -> grille 9x9.

7. L’ironie pédagogique - RE# valide ce qu’il ne peut produire

Nous avons maintenant les deux outils en main :

• Z3 (section 6) a produit la grille solution (le témoin) ;
• RE# (section 5) sait valider une ligne.

Faisons-les se rencontrer : extrayons chaque ligne de la solution produite par Z3, et vérifions-la avec RE#. Le vérificateur élégant certifie, en temps linéaire, la solution qu’il est lui-même incapable de produire.

using System.Diagnostics;
// Ironie : RE# valide CHAQUE ligne de la solution produite par Z3.
// Le verificateur elegant certifie - en temps lineaire - ce qu'il ne sait pas produire.
var lignesSolution = new string[9];
for (int r = 0; r < 9; r++) {
    char[] chars = new char[9];
    for (int c = 0; c < 9; c++) chars[c] = (char)('0' + solution[r, c]);
    lignesSolution[r] = new string(chars);
}
var sw = Stopwatch.StartNew();
int valides = 0;
foreach (var ligne in lignesSolution) {
    if (ligneValide.Matches(ligne).Length > 0) valides++;
}
sw.Stop();
Console.WriteLine($"RE# a verifie les 9 lignes de la solution Z3 en {sw.ElapsedTicks} ticks ({sw.ElapsedMilliseconds} ms).");
Console.WriteLine($"Lignes valides : {valides}/9");
Console.WriteLine();
Console.WriteLine("L'ironie : RE# certifie, plus vite que Z3 n'a resolu, une grille");
Console.WriteLine("qu'il ne SAURAIT PAS produire lui-meme (il est recognition-only).");
Console.WriteLine();
foreach (var ligne in lignesSolution) Console.WriteLine($"  {ligne} -> {(ligneValide.Matches(ligne).Length > 0 ? "VALIDE" : "invalide")}");

RE# a verifie les 9 lignes de la solution Z3 en 347960 ticks (34 ms).
Lignes valides : 9/9

L'ironie : RE# certifie, plus vite que Z3 n'a resolu, une grille
qu'il ne SAURAIT PAS produire lui-meme (il est recognition-only).

  534678912 -> VALIDE
  672195348 -> VALIDE
  198342567 -> VALIDE
  859761423 -> VALIDE
  426853791 -> VALIDE
  713924856 -> VALIDE
  961537284 -> VALIDE
  287419635 -> VALIDE
  345286179 -> VALIDE

Interprétation : le prestige va au vérificateur, le travail au résolveur

Double retournement :

1. Le reconnaisseur le plus élégant (RE#, temps linéaire) ne sait pas fabriquer la solution qu’il certifie.
2. Il la certifie en outre plus vite que la toolchain (Automata / intersection DFA) qui était censée être le reconnaisseur en 2020 - celle-la même qui explosait.

Le Sudoku donne à voir que matching (RE#) et solving (Z3) sont deux métiers. Le prestige du “rapide et élégant” va au vérificateur ; le travail dur - la production du témoin - reste irremplaçablement du côté de Z3. C’est la thèse de cette série, rendue concrète.

Exercice 2 : étendre l’encodage Z3 (Sudoku diagonal)

Objectif : Le Sudoku-X ajoute deux contraintes : les deux diagonales principales doivent aussi contenir 1..9 (tous distincts). Étendez la fonction ResoudreSudokuZ3 pour ajouter ces deux contraintes.

Indice : Récupérez les 9 IntExpr de la diagonale principale (cells[i,i]) et de l’anti-diagonale (cells[i, 8-i]), et ajoutez deux ctx.MkDistinct(...) supplémentaires avant s.Check().

Étape 1 : Écrivez une variante ResoudreSudokuXZ3 dans la cellule suivante.

// EXERCICE : ResoudreSudokuXZ3 (variante avec contraintes de diagonales)
// TODO etudiant : reprendre le schema de ResoudreSudokuZ3 et ajouter deux MkDistinct
// sur la diagonale principale (cells[i,i]) et l'anti-diagonale (cells[i, 8-i]).
public int[,] ResoudreSudokuXZ3(Context ctx, int[,] puzzle)
{
    return puzzle;  // TODO etudiant : remplacer par la resolution avec contraintes diagonales
}
Console.WriteLine("Exercice a completer : implementer les deux contraintes de diagonale.");

Exercice a completer : implementer les deux contraintes de diagonale.

8. Résoudre par toutes les voies - le banc d’essai

Jusqu’ici chaque barreau a été illustré isolément. Cette section les exécute côte à côte sur les mêmes grilles : la canonique (30 indices), la grille vide (0 indice) et une grille B à 26 indices. L’objectif n’est PAS de battre le résolveur optimal - l’optimum algorithmique du Sudoku, c’est Dancing Links (DLX), traité en détail dans les notebooks voisins de la série (Sudoku-02-DancingLinks en C#, et sa version Python ; cf. aussi le backtracking de Sudoku-01 et le Z3 dédié de Sudoku-12). Ici, l’objectif est que la discussion soit fertile : on tente toutes les résolutions, les bonnes comme les moins bonnes, et un échec honnête (timeout, faux négatif) en dit autant qu’une réussite.

Conway : deux artefacts à ne pas confondre

Le “Sudoku en un seul regex” de la lignée Conway existe en deux versions distinctes qu’on mélange souvent à tort :

Variante	Auteur	Mécanisme	Tourne sur
Monstre récursif	Damian Conway (2005), Davidebyzero	récursion PCRE (?R) / (?0) - non régulier	PCRE, module Python regex ; PAS System.Text.RegularExpressions
Variante déroulée	Aron Griffis (2007), domaine public	récursion déroulée en 81 blocs explicites : backrefs \1..\81 + lookaheads, aucun (?R)	tout moteur à backtracking : stdlib Python re et .NET

Le monstre récursif est l’anti-modèle du barreau 1 : élégant, illisible, et hors de portée du moteur .NET, qui ne sait pas faire de récursion de motif. (Le mécanisme (?R) est vérifiable en une ligne dans le module Python regex : \((?:[^()]|(?R))*\) reconnaît les parenthèses bien balancées - un langage non régulier - mais ne compile même pas en .NET.) C’est donc la variante déroulée de Griffis qu’on exécute ci-dessous en .NET : elle, au moins, tourne. La cellule génère les 81 blocs, puis résout par UNE substitution Regex.Replace - c’est le moteur de backtracking qui fait toute la recherche.

using System;
using System.Linq;
using System.Text;
using System.Diagnostics;
using System.Text.RegularExpressions;

// --- Generateur de la variante DEROULEE (Aron Griffis 2007, lignee Conway, domaine public) ---
// 81 blocs explicites, forward-check par lookahead, AUCUNE recursion (?R) : tourne en .NET.
int[] BlocDe(int i) { int x = i % 9, y = i / 9, b = (y / 3) * 27 + (x / 3) * 3;
    return new[] { b, b+1, b+2, b+9, b+10, b+11, b+18, b+19, b+20 }; }

string BuildSudokuRegex() {
    var re = new StringBuilder(); re.Append(@"\A"); re.Append("\n\n");
    for (int i = 0; i < 81; i++) {
        re.Append(@"\d*");
        var col = Enumerable.Range(0, i/9).Select(y => y*9 + (i%9));
        var row = Enumerable.Range(0, i%9).Select(x => (i/9)*9 + x);
        var blc = BlocDe(i).Where(c => c < i);
        var deja = col.Concat(row).Concat(blc).Distinct().OrderBy(z => z).ToList();
        if (deja.Count > 0) { re.Append(@"(?!" + string.Join("|", deja.Select(p => @"\" + (p+1))) + ")"); re.Append("\n"); }
        re.Append(@"(\d)"); re.Append("\n");                                                        // la case : on CAPTURE un chiffre
        re.Append(@"(?!(?:.*\n)+(?:.{10}){" + (i%9) + @"}\" + (i+1) + @"\b)"); re.Append("\n");      // pas ce chiffre dans la colonne en dessous
        re.Append(@"(?!\d*\ (?:.{10})*?\" + (i+1) + @"\b)"); re.Append("\n");                        // ni ailleurs apres, sur n'importe quelle ligne
        if (i%3 < 2) { re.Append(@"(?!\d*\ (?:.{10}){0," + (1 - i%3) + @"}\" + (i+1) + @"\b)"); re.Append("\n"); }
        if ((i/9)%3 < 2) { re.Append(@"(?!(?:.*\n){1," + (2 - (i/9)%3) + @"}(?:.{30}){" + ((i%9)/3) + @"}(?:.{10}){0,2}\" + (i+1) + @"\b)"); re.Append("\n"); }
        re.Append(@"\d*\s+"); re.Append("\n\n");
    }
    re.Append(@"\Z"); re.Append("\n"); return re.ToString();
}

// Resout par UNE substitution regex : c'est le moteur de backtracking qui fait la recherche.
(string grille, double ms) ResoudreParRegex(string puzzle, Regex rx) {
    string spread = Regex.Replace(puzzle, "[1-9]", "$0        ");  // chiffre + 8 espaces -> case large de 10
    string menu   = Regex.Replace(spread, "0", "123456789");       // case vide -> menu de candidats 1..9
    var repl = new StringBuilder();
    for (int r = 0; r < 9; r++) { for (int c = 0; c < 9; c++) { if (c > 0) repl.Append(' '); repl.Append("${" + (r*9+c+1) + "}"); } if (r < 8) repl.Append('\n'); }
    var sw = Stopwatch.StartNew();
    try {
        string outp = rx.Replace(menu, repl.ToString()); sw.Stop();
        bool solved = !outp.Replace(" ", "").Replace("\n", "").Contains("123456789");
        return (solved ? outp.Trim() : null, sw.Elapsed.TotalMilliseconds);
    } catch (RegexMatchTimeoutException) { sw.Stop(); return ("__TIMEOUT__", sw.Elapsed.TotalMilliseconds); }
}

string canon   = "5 3 0 0 7 0 0 0 0\n6 0 0 1 9 5 0 0 0\n0 9 8 0 0 0 0 6 0\n8 0 0 0 6 0 0 0 3\n4 0 0 8 0 3 0 0 1\n7 0 0 0 2 0 0 0 6\n0 6 0 0 0 0 2 8 0\n0 0 0 4 1 9 0 0 5\n0 0 0 0 8 0 0 7 9";
string vide    = string.Join("\n", Enumerable.Repeat("0 0 0 0 0 0 0 0 0", 9));
string grilleB = "0 4 5 0 1 0 0 0 0\n0 0 0 7 5 0 0 0 8\n0 0 7 0 8 0 0 1 0\n0 0 0 0 0 7 0 0 6\n6 8 0 0 0 0 0 7 2\n1 0 0 3 0 0 0 0 0\n0 6 0 0 7 0 8 0 0\n7 0 0 0 9 1 0 0 0\n0 0 0 0 3 0 4 5 0";

string pat = BuildSudokuRegex();

// Persiste l'artefact REEL : c'est LA "vraie chose" affichee tronquee en section 2 (cell 3).
// Le fichier committe en est byte-identique (même generateur), la regen est idempotente.
try {
    var dir = new[] { "assets", "MyIA.AI.Notebooks/Sudoku/assets" }.FirstOrDefault(System.IO.Directory.Exists) ?? "assets";
    System.IO.Directory.CreateDirectory(dir);
    System.IO.File.WriteAllText(System.IO.Path.Combine(dir, "sudoku-unrolled.regex.txt"), pat);
    Console.WriteLine($"Artefact sauvegarde : assets/sudoku-unrolled.regex.txt ({pat.Length} caracteres).");
} catch { Console.WriteLine("(assets/ en lecture seule : l'artefact committe fait foi)"); }

var rx = new Regex(pat, RegexOptions.IgnorePatternWhitespace, TimeSpan.FromSeconds(10));  // cap match 10 s = aveu d'echec honnete
Console.WriteLine($"Regex genere : {pat.Length} caracteres, 81 blocs, 0 recursion (?R).");
Console.WriteLine("Moteur : System.Text.RegularExpressions (.NET) ; cap match = 10 s.\n");

foreach (var (nom, puz) in new[] { ("canonique (30 indices)", canon), ("grille vide (0 indice)", vide), ("grille B (26 indices)", grilleB) }) {
    var (grille, ms) = ResoudreParRegex(puz, rx);
    string verdict = grille == "__TIMEOUT__" ? $"TIMEOUT (> {ms/1000:F0} s)"
                   : grille == null          ? $"PAS RESOLU - faux negatif en {ms:F0} ms"
                   :                            $"RESOLU en {ms:F1} ms";
    Console.WriteLine($"--- {nom} : {verdict} ---");
    Console.WriteLine(grille != null && grille != "__TIMEOUT__" ? grille + "\n" : "");
}

Artefact sauvegarde : assets/sudoku-unrolled.regex.txt (13515 caracteres).
Regex genere : 13515 caracteres, 81 blocs, 0 recursion (?R).
Moteur : System.Text.RegularExpressions (.NET) ; cap match = 10 s.

--- canonique (30 indices) : RESOLU en 3,0 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

--- grille vide (0 indice) : TIMEOUT (> 10 s) ---

--- grille B (26 indices) : PAS RESOLU - faux negatif en 788 ms ---

Le même regex, deux moteurs : la portabilité est une illusion

Le motif généré ci-dessus fait 13515 caractères et ne contient aucune récursion : il devrait donc se comporter pareil partout. Il n’en est rien. Le même motif, octet pour octet, appliqué en .NET (System.Text.RegularExpressions, cellule ci-dessus) et en Python (re, lignée PCRE, mesure reproductible hors notebook) diverge :

Grille	.NET System.Text.RegularExpressions	Python re
canonique (30 indices)	RESOLU (quasi-instantané)	RESOLU (quasi-instantané)
grille vide (0 indice)	TIMEOUT (> ~10 s)	RESOLU (quasi-instantané)
grille B (26 indices)	PAS RESOLU - faux négatif	RESOLU (~ 1 s)

Sur la grille canonique, les deux moteurs sont quasi-instantanés. Mais sur la grille vide il boucle jusqu’au cap de ~10 s, et sur la grille B il rend un faux négatif : il déclare “pas de solution” là où il en existe une que Python trouve. Les lookaheads d’optimisation que Griffis a réglés pour PCRE - \b, *? paresseux, sémantique du . face au saut de ligne - ne portent pas la même sémantique chez le backtracker .NET.

Leçon. Un regex de résolution par backtracking n’est pas portable : il est accordé à un moteur précis. Le “reconnaître != résoudre” du reste du notebook se double ici d’un “le même motif ne calcule pas la même chose selon le moteur”. (À l’opposé, la voie déclarative & -> théorie des chaînes, elle, est portable : le SMT-LIB émis se résout pareil partout où tourne Z3.)

Le monstre récursif (?R) : un troisième type de résultat - le rejet à la compilation

La variante déroulée ci-dessus ne contient aucune récursion : elle compile partout (et diverge selon le moteur, cf. tableau précédent). Mais les Sudoku-en-un-regex les plus célèbres - la lignée Conway, le noeud ikegami / PerlMonks 471168, les motifs de Davidebyzero - reposent eux sur la récursion (?R) / (?0) / (?&nom) : le motif s’appelle lui-même, ce qui décrit un langage non régulier (au sens strict, ce ne sont plus des “expressions régulières”).

Cette récursion donne une troisième sorte de “résultat”, à côté de résolu et timeout/faux-négatif : selon le moteur, le motif compile et tourne, ou bien il est rejeté d’emblée. Probe minimale et vérifiable - les parenthèses bien balancées (?<bal>\((?:[^()]|(?&bal))*\)), un langage non régulier classique - mesurée sur chaque moteur :

Moteur	Récursion (?R) / (?&nom)	Probe (()())	Probe (()
Python regex 2.5.140	supportée	MATCH	no
Perl 5.38.2	supportée	MATCH	no
PCRE2 10.42 (pcre2grep)	supportée	MATCH	no
Python re (stdlib 3.12)	rejetée	erreur de compilation (unknown extension ?R)	-
.NET System.Text.RegularExpressions	rejetée	exception à la construction (cellule suivante)	-

Mesure reproductible hors notebook (pcre2grep, perl, modules Python re / regex). Le monstre récursif de Sudoku est ce même mécanisme (?R) porté à 81 cases : élégant, illisible, et - point clé - hors de portée de .NET. C’est exactement pourquoi ce notebook exécute en .NET la variante déroulée (sans récursion), et non le monstre récursif.

using System;
using System.Text.RegularExpressions;

// Les Sudoku-en-un-regex CELEBRES (Conway, ikegami PerlMonks 471168, Davidebyzero) reposent sur la
// RECURSION (?R)/(?0)/(?&nom) - un langage NON regulier. .NET ne sait pas recurser un motif : il
// REJETTE la syntaxe à la construction. C'est le 3e type de "resultat" : ni resolu, ni timeout, mais
// motif impossible a compiler.
string[] recursifs = {
    @"\((?:[^()]|(?R))*\)",          // (?R)  : recursion du motif entier (style Conway/Davidebyzero)
    @"(?<g>\((?:[^()]|(?&g))*\))",   // (?&g) : recursion d'un sous-motif nomme
};
foreach (var motif in recursifs) {
    try {
        var _ = new Regex(motif);
        Console.WriteLine($"  COMPILE OK (inattendu) : {motif}");
    } catch (Exception ex) {
        Console.WriteLine($"  .NET REJETTE : {motif}");
        Console.WriteLine($"      -> {ex.GetType().Name}: {ex.Message}");
    }
}

Console.WriteLine();
Console.WriteLine("A l'inverse, la variante DEROULEE de Griffis (cellule plus haut) ne contient aucun (?R) :");
Console.WriteLine("c'est exactement pourquoi elle, elle COMPILE et tourne en .NET (avec les ecarts vus ci-dessus).");
Console.WriteLine("Lecon : 'le meme regex partout' est un mythe - la recursion est un dialecte PCRE, absent de .NET.");

  .NET REJETTE : \((?:[^()]|(?R))*\)
      -> RegexParseException: Invalid pattern '\((?:[^()]|(?R))*\)' at offset 14. Unrecognized grouping construct.
  .NET REJETTE : (?<g>\((?:[^()]|(?&g))*\))
      -> RegexParseException: Invalid pattern '(?<g>\((?:[^()]|(?&g))*\))' at offset 19. Unrecognized grouping construct.

A l'inverse, la variante DEROULEE de Griffis (cellule plus haut) ne contient aucun (?R) :
c'est exactement pourquoi elle, elle COMPILE et tourne en .NET (avec les ecarts vus ci-dessus).
Lecon : 'le meme regex partout' est un mythe - la recursion est un dialecte PCRE, absent de .NET.

using System;
using System.Linq;
using System.Diagnostics;

// Le contre-point : backtracking RECURSIF naif. La pile d'appels EST la pile de contexte
// (legere, zero allocation par essai). C'est l'outil qui epouse le substrat - et il est robuste.
bool Ok(int[] g, int i, int d) {
    int r = i/9, c = i%9, br = 3*(r/3), bc = 3*(c/3);
    for (int k = 0; k < 9; k++) if (g[r*9+k] == d || g[k*9+c] == d) return false;
    for (int dr = 0; dr < 3; dr++) for (int dc = 0; dc < 3; dc++) if (g[(br+dr)*9+bc+dc] == d) return false;
    return true;
}
bool Resoudre(int[] g) {
    int i = Array.IndexOf(g, 0); if (i < 0) return true;          // plus de case vide -> resolu
    for (int d = 1; d <= 9; d++) if (Ok(g, i, d)) { g[i] = d; if (Resoudre(g)) return true; g[i] = 0; }
    return false;                                                  // aucun chiffre ne passe -> on remonte (backtrack)
}
void Banc(string nom, string s81) {
    var g = s81.Where(ch => ch != ' ' && ch != '\n').Select(ch => (ch == '.' || ch == '0') ? 0 : ch - '0').ToArray();
    var sw = Stopwatch.StartNew(); bool ok = Resoudre(g); sw.Stop();
    Console.WriteLine($"{nom,-22} : {(ok ? "RESOLU" : "ECHEC")} en {sw.Elapsed.TotalMilliseconds:F1} ms");
}
Banc("canonique (30)", "53..7....6..195....98....6.8...6...34..8.3..17...2...6.6....28....419..5....8..79");
Banc("grille vide (0)", new string('.', 81));
Banc("grille B (26)",   "045010000000750008007080010000007006680000072100300000060070800700091000000030450");

canonique (30)         : RESOLU en 1,3 ms
grille vide (0)        : RESOLU en 0,1 ms
grille B (26)          : RESOLU en 3,2 ms

Annexe B — Le banc d’essai complet : tableaux consolidés

Toutes les voies, mesurées (kernel .net-csharp pour les lignes C#/.NET ; z3-py et Python re reproductibles hors notebook) :

Voie	Substrat	canon (30)	vide (0)	grille B (26)
Naïf récursif	C#	(mesure, voir section 8)	(mesure, voir section 8)	(mesure, voir section 8)
Naïf récursif	Python	(mesure, voir section 8)	(mesure, voir section 8)	(mesure, voir section 8)
Naïf récursif	NumPy	(mesure, voir section 8)	-	(mesure, voir section 8)
Regex déroulé	.NET	(mesure, voir section 8)	timeout (valeur de configuration)	faux négatif
même regex	Python re	(mesure, voir section 8)	(mesure, voir section 8)	(mesure, voir section 8)
P1 Z3 Distinct (entiers)	z3-py	(mesure, voir section 8)	(mesure, voir section 8)	(mesure, voir section 8)
P3 chaînes, appartenance fondue en re.inter / str.in_re	z3-py	unknown (au-delà d’une minute)	-	-
P3’’ chaînes, appartenance éclatée en str.contains (le regex se suffit)	.NET / z3-py	SAT (mesure, voir section 8)	-	-
P3’ chaînes, tous-distincts en inégalités 2 à 2	C# / z3-py	(mesure, voir section 8)	(mesure, voir section 8)	(mesure, voir section 8)
P2 DFA -> SMT	.NET (fork)	OOM à 81 (mur 1, cf. section 6b)	-	-
RE#	.NET	reconnaissance seule, aucun témoin	-	-
Monstre Conway (?R)	PCRE / Python regex	non régulier, absent de .NET	-	-
Dancing Links (DLX)	-	l’optimum (ordre de la microseconde) - cf Sudoku-02	-	-

Lecture : une valeur en ms/s = résolu ; TIMEOUT / faux négatif / unknown / OOM = échec honnête. P3, P3’’ et P3’ partagent le même substrat chaîne ; seule la forme d’émission du tous-distincts change : appartenance fondue en re.inter -> unknown ; même appartenance éclatée en str.contains -> SAT (mesure en section 6c) ; inégalités 2 à 2 -> (mesure, voir section 8, aussi en z3-py sur les trois grilles). Pour Z3 Distinct, la ligne est mesurée en z3-py ; le même encodage tourne en C# à la section 6 (~38 ms sur la canonique - rétablie par ré-exécution, valeur ponctuelle indicative).

Note sur les durées (mandat #9377/#9434) : les durées wall-clock et ratios quantitatifs exacts sont machine-dépendants par construction (compile .NET + JIT + GC, recompilation JAX côté Python, charge CPU du runner) et drainés de cette table de synthèse. Les résultats de résolution (résolu / SAT / TIMEOUT / unknown / OOM / faux négatif) et la tendance qualitative comparative (rapport d’ordres de grandeur, identification des échecs fertiles) sont reproductibles d’une exécution à l’autre et conservés. Les mesures exactes restent visibles dans les cellules de mesure amont (cell[26] “banc d’essai” — sortie de cellule 10 ; cell[31] “Z3 findet un témoin” — voir la sortie Elapsed, et la section 6c pour la mesure str.contains du 9x9). La pédagogie de cette cellule tient sur la différence qualitative entre les formes d’émission du tous-distincts (re.inter fondu vs str.contains éclaté), pas sur les ratios quantitatifs qui rebougent à chaque machine.

Quatre leçons fertiles - c’est la discussion, pas le chrono, qui est le livrable :

1. Le substrat compte autant que l’algorithme. Le même backtracking naïf fait un ordre de grandeur différent entre C# (pile d’appels légère, zéro allocation par essai), Python (interprété, alloc par appel) et NumPy (vectorisation inutile sur recherche séquentielle, surcoût par-élément à chaque accès scalaire). L’outil doit épouser le problème.

2. L’anti-modèle “gagne” puis s’effondre. Le regex déroulé est compétitif sur la canonique (du même ordre que le naïf C#, loin devant Z3) - puis il timeout sur la grille vide et rend un faux négatif sur la grille B. Rapide là où c’est facile, faux là où c’est dur : exactement le profil qu’on ne veut pas d’un résolveur.

3. Le naïf récursif est le vainqueur discret. Rapide et robuste sur les trois grilles, sans aucune machinerie symbolique. Le bon vieux backtracking, bien empilé en récursif, n’a pas du tout des performances médiocres - il bat même le regex sur la canonique. Les métaheuristiques (recuit, génétique) qui mettent plus d’une minute sur ce problème sont, ici, un contresens d’outil.

4. La voie symbolique atterrit - le 9x9 inclus - à condition de la bonne forme d’émission. Ce n’est pas “les voies élégantes explosent toujours” : c’est plus fin. P2 (DFA -> SMT) explose en états (mur 1, section 6b) ; P3 (appartenance fondue en re.inter) ne termine pas (unknown) ; mais la même appartenance éclatée en str.contains (P3’‘, le regex qui se suffit) atterrit la grille 9x9 complète, et les inégalités 2 à 2 (P3’) aussi - Distinct sur 81 entiers, qui n’en est que le sucre, est un résolveur de production encore plus rapide. Le critère décisif n’est ni le moteur ni le substrat (chaîne vs entier), c’est la forme d’émission de l’intersection : produit d’automates fondu (sature) vs primitive native éclatée (atterrit).

Synthèse du banc. Reconnaître (RE#) est linéaire et portable ; résoudre par appartenance fondue sature à l’échelle ; mais la même appartenance éclatée en str.contains - en restant un regex, 0 inégalité - atterrit le 9x9 ; les inégalités (chaînes P3’ ou entiers Distinct), et même un simple backtracking C#, atterrissent plus vite encore. La leçon transversale : choisir la bonne forme d’émission, pas le substrat le plus spectaculaire. Le DLX serait l’optimum (Sudoku-02), mais on ne cherchait pas l’optimum : on cherchait à comprendre pourquoi chaque voie réussit ou échoue. Voir les sections 6 et 6b (Z3 et le fork Automata) et 4-5 (RE# reconnaissance).

Tableau consolidant - le regex n’est PAS le mauvais outil

En croisant forme d’émission et moteur, le verdict est net : la voie symbolique atterrit réellement une grille de Sudoku - 4x4 et 9x9. Ce qui décide la réussite n’est ni le moteur, ni le substrat (chaîne vs entier), mais (a) la forme d’émission du tous-distincts et (b) la portabilité du dialecte.

Voie (forme d’émission)	Moteur	4x4	9x9	Nature du résultat
notre regex & -> appartenance fondue en re.inter	Z3 (fork Automata)	SAT (mesure, voir section 8)	unknown	atterrit le 4x4 ; le produit d’automates sature à 81
notre regex & -> appartenance éclatée en str.contains	Z3 (.NET)	SAT	SAT (mesure, voir section 8)	atterrit le 9x9 - 0 inégalité, le regex se suffit
mêmes chaînes, tous-distincts 2 à 2	Z3 (.NET)	SAT	SAT (mesure, voir section 8)	atterrit le 9x9 (mais quitte le regex)
Z3 Distinct (entiers, sucre du 2 à 2)	Z3	SAT	SAT (mesure, voir section 8)	résolveur de production
unrolled Griffis (substitution)	.NET	(mesure, voir section 8)	timeout / faux-neg	fragile, non portable
unrolled Griffis	Python re/regex, PCRE2, perl	solve (temps variables)	(idem)	portable mais fragile
monstre récursif (?R)	PCRE2 / perl / Python regex	récursion OK	-	dialecte PCRE
monstre récursif (?R)	.NET / Python re	rejet compile	-	non régulier, non portable
RE# (Resharp)	.NET	reconnaissance, aucun témoin	reconnaissance	vérifie, ne résout pas

Une matrice plus large (40+ moteurs : .NET, PCRE2, Perl, Python, Boost, RE2, std::regex, ICU, Rust, Java…) se compare commodément avec l’outil RegExpress (Viorel, v3.26) - utile pour voir la variété de comportements (?R) / lookbehind / backref d’un coup d’oeil. C’est une GUI Windows (WPF), non scriptable en headless : les lignes ci-dessus, elles, sont mesurées (in-notebook pour .NET/Z3/RE# ; pcre2grep/perl/Python reproductibles hors notebook). RegExpress est cité comme référence, pas reproduit ici.

Note sur les durées (mandat #9377/#9434) : les durées wall-clock de cette table sont machine-dépendantes par construction (compile Z3 + solver + charge CPU runner) et drainées. Les verdictis SAT/timeout/faux-neg/récursion/rejet/reconnaissance sont reproductibles d’une exécution à l’autre et conservés. Les mesures exactes restent visibles dans les cellules de mesure amont (section 6b et 6c, ainsi que le notebook parent 10 - Générer un témoin depuis A & ~B qui donne les ~100 ms pour le cas général). La tendance qualitative (atlas SAT vs unknown vs timeout vs rejet compile) est l’argument pédagogique : la décision qualitative résolu / non résolu discrimine la grille 9x9 entière, et se lit indépendamment des durées.

Verdict. Le regex atterrit : grille 4x4 complète depuis notre intersection &, et grille 9x9 complète dès qu’on éclate le tous-distincts en str.contains natif (0 inégalité, le regex se suffit). “Le mauvais outil” était un diagnostic trop court : le bon outil suit la forme d’émission (produit d’automates fondu vs primitive native) et le dialecte (la récursion PCRE n’est pas .NET).

Avis technique - la lignée Veanes et la “réécriture du parser”

L’intuition de l’auteur (“la réécriture du parser était sans doute au programme”) vise juste. Le fil rouge des travaux de Margus Veanes (MSR) est de sortir le front-end des regex de la construction d’automates pour le poser sur un raisonnement symbolique par dérivées :

• Rex / SFAz3 (années 2010, dans Automata) : regex -> automate symbolique (SFA) -> témoin via Z3. Puissant, mais c’est la voie qui cape le témoin (issue #6) et explose en produit d’automates (mur 1). C’est là où se trouvait le projet de 2020.
• SRM (“Symbolic Regex Matcher”, TACAS 2019) : remplace la construction de SFA par les dérivées symboliques - une réécriture du moteur de reconnaissance, rapide (classe RE2), qui deviendra le moteur non-backtracking de .NET 7. Recognition-only.
• dZ3 (“Symbolic Boolean Derivatives…”, PLDI 2021) : pousse les dérivées au cas booléen - résoudre directement A & ~B & ... dans Z3, soit exactement Ligne & Colonne & Bloc. C’est la brique qui résout sans matérialiser d’automate.
• RE# (POPL 2025) : ramène & / ~ en citoyens de première classe d’un matcher à dérivées, en temps linéaire - mais toujours reconnaissance, sans témoin.

Mon avis : la capacité que visait le projet (de l’intersection &/~ vers une grille résolue) n’a jamais été celle de SRM/RE# (reconnaissance), mais celle de la voie Z3 - d’abord SFAz3 (capée), puis la théorie des chaînes à la dZ3 (non capée, sans produit). La “réécriture du parser” qui débloque le 9x9, c’est précisément ce glissement : regex -> SFA devient regex -> contraintes SMT sur les chaînes - et, dernière marche, émettre chaque appartenance .*d.* comme la primitive native str.contains plutôt que de la fondre en re.inter. Le fork Automata (Epic #2979) câble enfin cette voie : &/~ en surface BREX, RegexToSMTConverter vers SMT-LIB 2.6, et le cap #6 levé. Bon repo, bonne idée, bon moment - il manquait la plomberie, désormais posée.

Synthèse - reconnaître != résoudre, et la forme d’émission décide

Les deux murs de 2020 étaient des murs de l’automate ; ils tombent ensemble dès qu’on change de moteur. Restait le 9x9, et c’est la forme d’émission de l’intersection qui le franchit : le regex, bien émis, atterrit réellement la grille - sans une seule inégalité.

	RESOUDRE (produire la grille)	VERIFIER (valider une grille remplie)
Folklore PCRE (backtracking)	détour de backtracking, illisible	monstrueux
BREX/Rex + SFAz3 (2020)	muré (cap ~21 char, issue #6 ; explosion du produit)	explosion DFA
& -> chaînes Z3, appartenance fondue en re.inter	témoin non-capé, sans produit ; atterrit le 4x4, unknown au 9x9	(oui)
& -> chaînes Z3, appartenance éclatée en str.contains	atterrit la grille 9x9 complète (~53 s) - 0 inégalité, le regex se suffit	(oui)
chaînes Z3, tous-distincts en inégalités 2 à 2	atterrit la grille 9x9 complète (~0,8 s ; quitte le regex)	(oui)
RE# (2025)	recognition-only, aucun témoin	temps linéaire
Z3 Distinct (81 entiers)	résolveur de production (~38 ms)	-

Leçon : décrire une contrainte par intersection régulière (Ligne & Colonne & Bloc) est une représentation élégante qui atterrit la grille - 4x4 complète, et 9x9 complète sans quitter l’appartenance régulière. Ce qui décide la réussite n’est ni le moteur (DFA vs dérivées vs SMT) ni le substrat (chaîne vs entier), mais la forme d’émission du tous-distincts : fondu en un produit d’automates (re.inter/str.in_re), il sature à l’échelle des 27 groupes qui se chevauchent ; éclaté en la primitive native str.contains (= .*d.* par chiffre), il atterrit - et les inégalités 2 à 2 (dont Distinct est le sucre) plus vite encore, mais hors du regex. RE# en est le vérificateur linéaire, pas le solveur ; l’ironie (RE# valide plus vite qu’il ne produit) est le pont entre cette série Sudoku et la série Z3 (Epic #1206).

La chaîne moderne (section 6b, et notebook 10 de la série Z3) fait tomber les deux murs de 2020 : &/~ compile vers la théorie des chaînes de Z3, qui ne cape aucun témoin et ne construit aucun produit d’automates. Le revers n’est donc pas “Z3 string-theory ne sait pas faire le Sudoku” - il le fait, le 9x9 inclus (cf section 6c) - mais “il faut émettre l’appartenance dans la bonne forme : str.contains natif, pas re.inter fondu”.

Le banc d’essai (section 8 ci-dessus) confirme empiriquement chaque case de ce tableau : le regex déroulé s’effondre (timeout, faux négatif), la voie chaînes-en-appartenance-fondue fait unknown, la même appartenance éclatée en str.contains (P3’‘) et les inégalités (P3’) et Distinct atterrissent, et le backtracking C# naïf est le vainqueur discret. Le DLX, lui, est l’optimum dédié : cf Sudoku-02-DancingLinks.

Footnote d’homonymie : Damian Conway (luminaire des regex Perl, dont relève le folklore du barreau 1) n’est pas John Conway (le Game of Life, hero de notre série Lean #2162). Les deux Conway se croisent dans ce notebook.

Les tableaux consolidés du banc d’essai complet sont en annexe B ; les cadres théoriques qui expliquent pourquoi la forme d’émission décide (M2L-str, décomposition monadique de Veanes) en annexe A.

Annexe S10 - Pont Microsoft.Z3 natif : l’automate symbolique, sans detour

Grain DEEP/notebook-dotnet, lane myia-po-2023:CoursIA-2, prev: DEEP/notebook-dotnet #10450

Contexte : la fiche de parite scripts/notebook_tools/twin_pairs.d/sudoku-13-symbolicautomata.yaml porte aujourd’hui bridge_verdict: INTRINSIC au motif que “le C# (pur System.* stdlib, 0 NuGet, 18 cellules code) construit la logique d’automate symbolique from scratch”. L’omission est la suivante : le notebook utilise deja Microsoft.Z3 (cellule 17, NuGet officiel, axe 1 du registre #3801), et il resout des contraintes d’automates symboliques dans la theorie des chaines - uniquement en passant par le fork Automata (cellule 21) ou par ParseSMTLIB2String textuel (cellule 26). Cette annexe exhibe le constructeur d’automate symbolique directement emit en SMT-LIB 2.6 par concatenation C# depuis le notebook, et le moteur Microsoft.Z3 qui le resout - sans fork Automata, sans lib externe, juste la lib officielle Microsoft.Z3 et la theorie des chaines Z3.

Ce que cette annexe prouve : sous l’angle axe 1 (binding .NET / NuGet officiel), Microsoft.Z3 est atteignable et rejoint des contraintes d’automates symboliques. Le verdict precedent (“INTRINSIC pour limite academique SFAz3+Z3 ‘monstre regex tronque’”) reste valide en second niveau (la limite SFAz3/Z3 existe, cap du temoin a ~21 caracteres sans le detour par la theorie des chaines : voir known_differences du yaml) mais n’est plus de premier niveau. Le triptyque devient :

Niveau	Verdict	Motif
Premier (ce qu’on ajoute)	RECOVERABLE-LOCAL	la lib Microsoft.Z3 (NuGet, chargee par cellule 17) resout la theorie des chaines, donc la contrainte d’automate symbolique via str.in_re. Pont direct .NET -> SMT-LIB 2.6 -> temoin.
Second (connu_differences)	plafond SFAz3+Z3 “monstre regex tronque”	la limite est academique et documentee (cap du temoin ~21 caracteres SFAz3, voir issue upstream AutomataDotNet/Automata#6), pas un workaround degrade. Ce plafond vit dans known_differences du yaml.

Ce que cette annexe ne fait PAS : remplacer la voie from-scratch (cellules 5-7) ou la voie fork Automata (cellule 21). Le from-scratch garde sa valeur pedagogique (reconnaissance de l’explosion DFA), le fork Automata reste le pont avec & / ~ first-class. Cette annexe est en plus, jamais a la place - mandat #10382 (parite lib-vs-lib).

Lecture que cette annexe referme

Le titre du notebook est “Le Sudoku comme Regex Symbolique”. Il a resolu la promesse via SMT-LIB 2.6 emis par fork Automata (cellule 21) ou via emmission manuelle (cellule 26). Il manquait un troisieme chemin : construire un terme regex SMT-LIB 2.6 directement depuis C# (StringBuilder), le passer a Microsoft.Z3.Context.ParseSMTLIB2String (API native), et le resoudre. Ce chemin montre que la lib Microsoft.Z3 elle-meme - sans fork Automata - tient le role de constructeur d’automate symbolique : la representation reguliere (re.++, re.*, re.inter, re.range) est un terme SMT-LIB 2.6 direct, et la theorie des chaines le resout.

// === Annexe S10 : constructeur d'automate symbolique direct via Microsoft.Z3 (SMT-LIB 2.6 emis en C#) ===
// Ce que cette cellule montre : la theorie des chaines Z3 (regex SMT-LIB 2.6) tient le role de
// **constructeur d'automate symbolique**. On emet le terme regex PAR CONCATENATION C# (un
// compilateur SMT-LIB inline) ; le moteur Microsoft.Z3 le resout et fournit le temoin.
// Aucune dependance externe (pas de fork Automata) : juste la lib Microsoft.Z3 officielle.
// (Cellule auto-suffisante : charge Z3 ellememe au lieu de dependre de la cellule 17.)
#r "../SymbolicAI/SMT/Z3.Linq/.deploy/Microsoft.Z3.dll"
using Microsoft.Z3;
using System.IO;
using System.Runtime.InteropServices;
using System.Text;

// --- Z3 est une librairie native (libz3.dll) ; on la résout a cote du Microsoft.Z3.dll charge.
// (Try/catch : en run de bout en bout, la cellule de chargement Z3 a deja pose LE resolver
//  autorise par assembly ; en run isole, cette cellule reste auto-suffisante et le pose elle-meme.)
try {
NativeLibrary.SetDllImportResolver(typeof(Context).Assembly, (name, assembly, path) => {
    if (name == "libz3") {
        string asmDir = Path.GetDirectoryName(typeof(Context).Assembly.Location);
        string[] cands = {
            Path.Combine(asmDir ?? ".", "libz3.dll"),
            Path.GetFullPath("../SymbolicAI/SMT/Z3.Linq/.deploy/libz3.dll"),
            "../SymbolicAI/SMT/Z3.Linq/.deploy/libz3.dll"
        };
        foreach (var c in cands) if (File.Exists(c) && NativeLibrary.TryLoad(c, out IntPtr h)) return h;
    }
    return IntPtr.Zero;
});
} catch (InvalidOperationException) {
    Console.WriteLine("(resolver libz3 deja pose par la cellule de chargement Z3 - run sequentiel, resolution reutilisee)");
}
var ctx = new Context();
Console.WriteLine($"Z3 charge. Version {Microsoft.Z3.Version.FullVersion}.\n");

// --- Contrainte : "1 apparait avant 2, 2 avant 3, ..., 8 avant 9", au moins une fois chacun.
// Temoin le plus court : "123456789". En SMT-LIB 2.6 : concat alternant (re.* .) et (str.to_re d).
var sb = new StringBuilder();
sb.Append("(re.++ ");
for (int d = 1; d <= 9; d++) {
    sb.Append("(re.* (re.range \"0\" \"9\")) ");
    sb.Append($"(str.to_re \"{d}\") ");
}
sb.Append("(re.* (re.range \"0\" \"9\")))");
string regexTerm = sb.ToString();
string script = "(declare-const w String)\n(assert (str.in_re w " + regexTerm + "))\n(check-sat)";

Console.WriteLine("Terme regex SMT-LIB 2.6 emis en C# (compilateur SMT-LIB inline) :");
Console.WriteLine("  " + regexTerm);
Console.WriteLine($"  ({regexTerm.Length} caracteres, 0 fork Automata, 0 NuGet supplementaire - juste Microsoft.Z3, axe 1 du registre #3801)\n");

var sw = System.Diagnostics.Stopwatch.StartNew();
var asserts = ctx.ParseSMTLIB2String(script);
var solver = ctx.MkSolver();
solver.Assert(asserts);
var status = solver.Check();
sw.Stop();

Console.WriteLine($"Z3 (Microsoft.Z3, theorie des chaines, str.in_re) : {status} en {sw.Elapsed.TotalMilliseconds:F0} ms");
if (status == Status.SATISFIABLE) {
    var w = (SeqExpr)ctx.MkConst("w", ctx.StringSort);
    string temoin = solver.Model.Eval(w, true).ToString().Trim('"');
    Console.WriteLine($"Temoin (chaine reconnue par l'automate symbolique) : \"{temoin}\" ({temoin.Length} char)");
    bool sousSeqOK = true;
    int idx = -1;
    for (int d = 1; d <= 9; d++) {
        int next = temoin.IndexOf((char)('0' + d), idx + 1);
        if (next < 0) { sousSeqOK = false; break; }
        idx = next;
    }
    Console.WriteLine($"Sous-sequence ordonnee 1..9 verifiee : {sousSeqOK} (caracteres n'importe ou, ordre croissant)");
    Console.WriteLine();
    Console.WriteLine("**PONT .NET -> Microsoft.Z3 (automate symbolique) : OK**");
    Console.WriteLine("  - axe 1 (binding .NET / NuGet officiel) : Microsoft.Z3, charge par #r en cellule 17 ou 47, registre #3801");
    Console.WriteLine("  - theorie des chaines Z3 : str.in_re / re.++ / re.* / re.range / str.to_re -> temoin");
    Console.WriteLine("  - sortie commitee : voir exec_count + outputs de cette cellule");
} else {
    Console.WriteLine($"Statut inattendu : {status}");
}

(resolver libz3 deja pose par la cellule de chargement Z3 - run sequentiel, resolution reutilisee)
Z3 charge. Version Z3 4.12.2.0.

Terme regex SMT-LIB 2.6 emis en C# (compilateur SMT-LIB inline) :
  (re.++ (re.* (re.range "0" "9")) (str.to_re "1") (re.* (re.range "0" "9")) (str.to_re "2") (re.* (re.range "0" "9")) (str.to_re "3") (re.* (re.range "0" "9")) (str.to_re "4") (re.* (re.range "0" "9")) (str.to_re "5") (re.* (re.range "0" "9")) (str.to_re "6") (re.* (re.range "0" "9")) (str.to_re "7") (re.* (re.range "0" "9")) (str.to_re "8") (re.* (re.range "0" "9")) (str.to_re "9") (re.* (re.range "0" "9")))
  (411 caracteres, 0 fork Automata, 0 NuGet supplementaire - juste Microsoft.Z3, axe 1 du registre #3801)

Z3 (Microsoft.Z3, theorie des chaines, str.in_re) : SATISFIABLE en 107 ms
Temoin (chaine reconnue par l'automate symbolique) : "123456789" (9 char)
Sous-sequence ordonnee 1..9 verifiee : True (caracteres n'importe ou, ordre croissant)

**PONT .NET -> Microsoft.Z3 (automate symbolique) : OK**
  - axe 1 (binding .NET / NuGet officiel) : Microsoft.Z3, charge par #r en cellule 17 ou 47, registre #3801
  - theorie des chaines Z3 : str.in_re / re.++ / re.* / re.range / str.to_re -> temoin
  - sortie commitee : voir exec_count + outputs de cette cellule

Interpretation - ce qu’on vient de voir

Trois choses, mesurees :

1. Le constructeur d’automate symbolique tient en C# de 8 lignes. Le terme regex SMT-LIB 2.6 (re.++ (re.* (re.range "0" "9")) (str.to_re "1") ... (re.* (re.range "0" "9"))) est ici emis par concatenation StringBuilder - c’est un compilateur SMT-LIB minimal pour la theorie des chaines. Pont direct .NET -> SMT-LIB 2.6, sans detour.

2. Microsoft.Z3 resout, et le temoin est immediat. Le solveur de chaines Z3 reconnait en millisecondes que le langage regulier decrit (sous-sequence ordonnee 1..9) est habite, et produit un temoin. La these du notebook (“le regex, bien emis, est l’outil”) est demontree a nouveau, par une autre emmission de la meme contrainte.

3. Pas de fork Automata, pas de cell 21. Le Pont utilise exclusivement Microsoft.Z3 (cellule 17, NuGet, axe 1 registre #3801), Context.ParseSMTLIB2String (API native) et la theorie des chaines Z3. C’est la lib Microsoft.Z3 qui est le moteur, pas un wrapper autour d’un autre solveur.

Pourquoi le verdict change de niveau

La fiche de parite scripts/notebook_tools/twin_pairs.d/sudoku-13-symbolicautomata.yaml porte bridge_verdict: INTRINSIC au motif que “le C# construit la logique d’automate symbolique from scratch”. La clause “from scratch” est vraie en l’etat du depot avant cette annexe : le notebook C# utilise Microsoft.Z3 pour la resolution (cellule 18, Distinct sur 81 entiers) mais deleguait la construction d’automate au fork Automata (cellule 21) ou a un SMT-LIB 2.6 ecrit a la main (cellule 26). L’annexe referme cette brèche : la lib est bien employee pour les deux roles. Le verdict devient :

• Premier niveau (registre modifie) : RECOVERABLE-LOCAL - la lib Microsoft.Z3 (NuGet, axe 1 du registre #3801) resout des contraintes d’automates symboliques via la theorie des chaines. Le C# n’est pas “from scratch” pour la theorie des chaines : il l’invoque.
• Second niveau (known_differences, inchange) : la limite SFAz3+Z3 “monstre regex tronque” reste vraie (cap du temoin ~21 caracteres sur le chemin SFAz3 d’origine, voir issue AutomataDotNet/Automata#6). Cette limite est academique et documentee, pas un workaround degrade - c’est pourquoi elle vit dans known_differences du yaml, pas dans bridge_verdict.

Mirroir du precedent GT-17 (#10464)

Meme structure a deux niveaux : - Premier niveau : la lib est atteignable (axe 1 NuGet = RECOVERABLE-LOCAL). - Second niveau : la limite “monstre regex tronque” est partagee par les deux jumeaux (pas un defaut de parite).

From-scratch from-scratch (cellules 5-7) et fork Automata (cellule 21) restent en place. Le pont est en plus, jamais a la place.

Exercice 3 : classifier recognition vs solving (conceptuel)

Objectif : Pour chacune des tâches ci-dessous, indiquez quel outil convient (RE# pour la reconnaissance / vérification, Z3 pour la résolution / production de témoin) et pourquoi.

Tâche	Outil attendu	Pourquoi
(a) Vérifier qu’une grille remplie respecte les règles	RE#	…
(b) Résoudre un puzzle à partir de cases vides	Z3	…
(c) Vérifier qu’une chaîne est un nombre à 9 chiffres distincts	…	…
(d) Trouver une permutation de 1..9 maximisant un critère	…	…

Indice : Posez-vous : la tâche demande-t-elle de produire une solution (solving -> Z3) ou seulement de reconnaître si une entrée donnée est valide (matching -> RE#) ?

// EXERCICE (conceptuel) : classifier recognition (RE#) vs solving (Z3).
// TODO etudiant : completer le tableau avec l'outil et la justification.
Console.WriteLine("Exercice a completer : pour chaque tache, indiquer RE# ou Z3 et pourquoi.");
Console.WriteLine();
Console.WriteLine("(a) Verifier qu'une grille remplie respecte les regles : RE#  -> ...");
Console.WriteLine("(b) Resoudre un puzzle a partir de cases vides       : Z3  -> ...");
Console.WriteLine("(c) Verifier qu'une chaine = 9 chiffres distincts    : ... -> ...");
Console.WriteLine("(d) Trouver une permutation de 1..9 maximisant un critere : ... -> ...");

Exercice a completer : pour chaque tache, indiquer RE# ou Z3 et pourquoi.

(a) Verifier qu'une grille remplie respecte les regles : RE#  -> ...
(b) Resoudre un puzzle a partir de cases vides       : Z3  -> ...
(c) Verifier qu'une chaine = 9 chiffres distincts    : ... -> ...
(d) Trouver une permutation de 1..9 maximisant un critere : ... -> ...

Annexe S11 - Pont PythonNet vers dd : le BDD du jumeau Python, le même moteur

La section 9 du jumeau Python compile la contrainte de ligne mini-Sudoku en diagramme de décision binaire (BDD) avec la librairie dd (PyPI). Sudoku-14 construit ses BDD from scratch en C# pur ; cette annexe prend le chemin complémentaire : sans réimplémenter le moteur, elle invoque le même dd.autoref.BDD que le jumeau Python via le pont .NET -> pythonnet -> CPython (axe 5 du registre #3801 : « la lib a-t-elle un binding Python ? » — ici le pont va le chercher).

Un BDD est un automate déterministe acyclique : chaque variable booléenne est un niveau de branchement (vrai/faux), les feuilles sont 0 (rejet) ou 1 (acceptation). La vertu : un BDD factorise une table de vérité exponentielle (2^n lignes) en un graphe souvent polynomial, puis répond reconnaissance et dénombrement en temps linéaire en sa taille.

L’encodage est l’encodage verbatim du jumeau Python : ligne mini-Sudoku de 3 cellules, chiffres 1 à 3, tous distincts ; chaque chiffre tient sur 2 bits, donc 3 cellules = 6 variables booléennes (c0_b0 à c2_b1), et la table de vérité brute fait 2^6 = 64 lignes. Nous mesurons la taille du BDD compilé, le dénombrement exact des lignes valides et un modèle extrait — puis nous contre-vérifions par l’énumération exhaustive des 64 lignes, menée indépendamment côté C# et côté Python : le BDD doit retrouver exactement les 6 permutations de (1, 2, 3).

Prérequis d’exécution : la variable d’environnement PYTHONNET_PYDLL doit pointer vers une DLL CPython hébergeant dd épinglé (pip install dd==0.6.0). Ce notebook ne hardcode aucun chemin machine (précédent Search-7) ; la cellule échoue explicitement si la variable est absente.

#r "nuget: pythonnet,3.1.0"
using Python.Runtime;
using System;
using System.Collections.Generic;
using System.IO;

// === Annexe S11 : pont PythonNet -> dd.autoref.BDD, LE MÊME MOTEUR que le jumeau Python (section 9) ===
// Cycle de vie validé (précédents Search-7 / Search-10 / Sudoku-5) : CPython hébergé dans le kernel
// .NET Interactive, bloc GIL UNIQUE dans cette cellule, tout le calcul côté Python, les résultats
// reviennent par Get<string>. Pas de PythonEngine.Shutdown() : sur .NET 10 il lève BinaryFormatter
// et tuerait le kernel persistant dont dépendent les cellules suivantes ; le moteur reste
// initialisé, le GIL est libéré en fin de bloc (précédent Search-7).
var pyDll = Environment.GetEnvironmentVariable("PYTHONNET_PYDLL");
if (string.IsNullOrEmpty(pyDll) || !File.Exists(pyDll))
    throw new InvalidOperationException(
        "Variable d'environnement PYTHONNET_PYDLL absente ou invalide. Pointez-la vers la DLL " +
        "CPython hébergeant dd (pip install dd==0.6.0) ; ce notebook refuse de hardcoder un chemin machine.");
// Résolution des DLL dépendantes : le répertoire de CPython précède le PATH (calculé, jamais affiché).
var pyDir = Path.GetDirectoryName(Path.GetFullPath(pyDll));
Environment.SetEnvironmentVariable(
    "PATH", pyDir + Path.PathSeparator + Environment.GetEnvironmentVariable("PATH"));

// --- Contre-vérification C# (avant le pont) : énumération EXHAUSTIVE des 64 lignes, sans BDD ---
var lignesBrutes = new List<(int D0, int D1, int D2)>();
for (int n = 0; n < 64; n++)
{
    var t = (D0: n & 3, D1: (n >> 2) & 3, D2: (n >> 4) & 3);
    if (t.D0 >= 1 && t.D0 <= 3 && t.D1 >= 1 && t.D1 <= 3 && t.D2 >= 1 && t.D2 <= 3
        && t.D0 != t.D1 && t.D0 != t.D2 && t.D1 != t.D2)
        lignesBrutes.Add(t);
}
lignesBrutes.Sort();
Console.WriteLine($"Énumération exhaustive C# : {lignesBrutes.Count} lignes valides sur 64");
Console.WriteLine();

Runtime.PythonDLL = pyDll;
PythonEngine.Initialize();
Console.WriteLine($"Pont PythonNet : .NET -> CPython {PythonEngine.Version} -> dd.autoref.BDD (même moteur que le jumeau Python)");
Console.WriteLine();

using (Py.GIL())
{
    dynamic scope = Py.CreateScope();
    scope.Exec(@"
import importlib.metadata as md
from dd.autoref import BDD

version_dd = md.version('dd')
assert version_dd == '0.6.0', 'pin de reproductibilité : dd==0.6.0 attendu, %s installé' % version_dd

b = BDD()
# 3 cellules, 2 bits chacune (chiffre 1..3 encodé sur b0, b1) -- encodage verbatim du jumeau Python.
b.declare('c0_b0','c0_b1','c1_b0','c1_b1','c2_b0','c2_b1')

def cellule_egale(ci, d):
    # Expression booléenne : la cellule ci vaut le chiffre d (1..3).
    return ' & '.join('(%sc%d_b%d)' % ('' if ((d >> bi) & 1) else '!', ci, bi) for bi in range(2))

def cellule_dans_domaine(ci):
    # La cellule ci vaut 1, 2 ou 3 (exclut le 0 hors-domaine).
    return ' | '.join('(%s)' % cellule_egale(ci, d) for d in range(1, 4))

# Domaine : chaque cellule dans {1, 2, 3}
domaine = ' & '.join('(%s)' % cellule_dans_domaine(ci) for ci in range(3))

# Distinction : chaque paire de cellules diffère sur au moins un bit
paires_diff = []
for ci in range(3):
    for cj in range(ci + 1, 3):
        xors = ['((c%d_b%d & !c%d_b%d) | (!c%d_b%d & c%d_b%d))' % (ci, bi, cj, bi, ci, bi, cj, bi)
                for bi in range(2)]
        paires_diff.append('(' + ' | '.join(xors) + ')')
distinct = ' & '.join(paires_diff)

# L'automate symbolique compilé = le BDD de (domaine ET distinct)
u_ligne_valide = b.add_expr('(%s) & (%s)' % (domaine, distinct))

nb_noeuds = len(b)
nb_solutions = b.count(u_ligne_valide, nvars=6)
un_modele = b.pick(u_ligne_valide)

def decoder(assign):
    # dict de bits -> triplet de chiffres décodés (d0, d1, d2)
    return tuple(sum(int(assign['c%d_b%d' % (ci, bi)]) << bi for bi in range(2)) for ci in range(3))

lignes1 = []
lignes1.append('Variables booléennes : 6 (3 cellules x 2 bits)')
lignes1.append('Table de vérité brute : 2^6 = %d lignes' % 2 ** 6)
lignes1.append('BDD compilé            : %d noeuds (graphe factorisé)' % nb_noeuds)
lignes1.append('Lignes valides         : %d  (attendu 3! = 6)' % nb_solutions)
lignes1.append('Un modèle (BDD.pick)   : %s  (décodé : %s)' % (un_modele, decoder(un_modele)))
lignes1.append('moteur : dd %s, même encodage et mêmes chiffres que le jumeau Python' % version_dd)
summary1 = chr(10).join(lignes1)

# --- Contre-vérification exhaustive côté Python : les 64 lignes balayées à la brute ---
valides_brut = set()
for n in range(64):
    assign = dict(('c%d_b%d' % (ci, bi), bool((n >> (2 * ci + bi)) & 1))
                  for ci in range(3) for bi in range(2))
    d = decoder(assign)
    if all(x in (1, 2, 3) for x in d) and len(set(d)) == 3:
        valides_brut.add(d)
modeles_bdd = sorted(decoder(m) for m in b.pick_iter(u_ligne_valide))
lignes2 = []
lignes2.append('Énumération exhaustive des 64 lignes (côté Python, sans BDD) : %d valides' % len(valides_brut))
lignes2.append('Extraction BDD (pick_iter) : %d modèles' % len(modeles_bdd))
lignes2.append('Les deux listes coïncident : %s' % (sorted(valides_brut) == modeles_bdd))
summary2 = chr(10).join(lignes2)

lignes_valides = ', '.join(str(t) for t in modeles_bdd)
");
    Console.WriteLine(scope.Get<string>("summary1"));
    Console.WriteLine();
    Console.WriteLine(scope.Get<string>("summary2"));
    Console.WriteLine();
    string brutPython = scope.Get<string>("lignes_valides");
    string brutCsharp = string.Join(", ", lignesBrutes);
    bool accord = brutPython == brutCsharp;
    Console.WriteLine($"Accord exhaustif C# <-> BDD : {accord}");
    Console.WriteLine("  C#  (64 lignes balayées) : " + brutCsharp);
    Console.WriteLine("  BDD (pick_iter)          : " + brutPython);
    Console.WriteLine();
    Console.WriteLine("Le C# a piloté dd par l'API du scope (Exec + Get<string>) : même moteur, même encodage, mêmes chiffres que le jumeau Python.");
}

Installing Packages

• pythonnet

Énumération exhaustive C# : 6 lignes valides sur 64

Pont PythonNet : .NET -> CPython 3.13.12 | packaged by Anaconda, Inc. | (main, Feb 24 2026, 16:05:56) [MSC v.1942 64 bit (AMD64)] -> dd.autoref.BDD (même moteur que le jumeau Python)

Variables booléennes : 6 (3 cellules x 2 bits)
Table de vérité brute : 2^6 = 64 lignes
BDD compilé            : 90 noeuds (graphe factorisé)
Lignes valides         : 6  (attendu 3! = 6)
Un modèle (BDD.pick)   : {'c0_b0': False, 'c0_b1': True, 'c1_b0': True, 'c1_b1': False, 'c2_b0': True, 'c2_b1': True}  (décodé : (2, 1, 3))
moteur : dd 0.6.0, même encodage et mêmes chiffres que le jumeau Python

Énumération exhaustive des 64 lignes (côté Python, sans BDD) : 6 valides
Extraction BDD (pick_iter) : 6 modèles
Les deux listes coïncident : True

Accord exhaustif C# <-> BDD : True
  C#  (64 lignes balayées) : (1, 2, 3), (1, 3, 2), (2, 1, 3), (2, 3, 1), (3, 1, 2), (3, 2, 1)
  BDD (pick_iter)          : (1, 2, 3), (1, 3, 2), (2, 1, 3), (2, 3, 1), (3, 1, 2), (3, 2, 1)

Le C# a piloté dd par l'API du scope (Exec + Get<string>) : même moteur, même encodage, mêmes chiffres que le jumeau Python.

Lecture : le même moteur, la même preuve - et le plafond honnête

Mesuré, et identique au jumeau Python : le BDD compile la table de vérité de 64 lignes en 90 nœuds, dénombre exactement les 6 lignes valides (les 3! permutations de (1, 2, 3)) sans les énumérer, et extrait un modèle par simple descente (pick -> (2, 1, 3)). L’accord exhaustif referme la boucle : l’énumération brute des 64 lignes, menée indépendamment côté C# et côté Python, retrouve exactement les 6 permutations que le pick_iter du BDD extrait du graphe — les trois voies (brute C#, brute Python, BDD) disent la même chose.

Le plafond honnête (même mise en garde que le jumeau) : cet exemple tient en 6 variables ; la contrainte « tous-distincts » est dure pour les BDD — sur la vraie ligne Sudoku (9 cellules, 4 bits chacune = 36 variables), le BDD explose à plusieurs millions de nœuds (constat voisin dans le MDD from-scratch de Sudoku-14). C’est précisément pour cela que Z3 n’utilise pas un BDD brut pour le Sudoku : sa théorie spécialisée des entiers (Distinct, arithmétique) est bien plus compacte qu’une explosion booléenne. Le BDD reste l’outil de choix pour la logique purement booléenne (circuits, model-checking) ; le solveur SMT règne sur l’arithmétique.

Pont avec le jumeau Python. La section 9 du jumeau exécute dd en natif ; cette annexe atteint le même moteur (dd 0.6.0 épinglé) par pythonnet 3.1.0 — parité de moteur, pas réimplémentation : les deux jumeaux affichent les mêmes chiffres (90 nœuds, 6 lignes valides, modèle (2, 1, 3)) dans leurs outputs commités, preuve cross-twin de l’encodage.

---

9. Références & connexions

Sources primaires

• Folklore “Sudoku en un regex” (tradition Perl) - ikegami, PerlMonks 2005 (solveur via le moteur regex avec blocs de code embarqués) ; module pur-regex Regexp::Sudoku d’Abigail. Le monstre PCRE (barreau 1), en formes récursive (?R) (hors .NET) et déroulée (tourne en .NET).
• Forme déroulée (générateur) - Aron Griffis, Sudoku with a Perl regular expression (2007), domaine public : les 81 blocs explicites (lookaheads + backreferences, sans (?R)) que nous régénérons et exécutons en section 8 (artefact assets/sudoku-unrolled.regex.txt).
• Issue upstream AutomataDotNet/Automata#6 (créée 2020-12-07, toujours sans réponse) : cap du témoin à ~21 caractères (barreau 2, mur 2).
• Margus Veanes et al., Derivative-based nonbacktracking real-world regex matching - MSR-TR-2020-25 (août 2020). Le papier contemporain de la tentative 2020.
• Margus Veanes, Symbolic Automata (exposé de référence, Dagstuhl Seminar 17142, avril 2017) : le programme ” automates symboliques ” au complet - SFA sur une algèbre de Boole effective, minimisation symbolique (D’Antoni & Veanes, Minimization of Symbolic Automata, POPL’14 ; bisimulation-avant TACAS’17 ; le cas ” Sometimes Moore is Less ” y documenté l’explosion de déterminisation, soit le mur 1 de ce notebook), logique M2L-str vers SFA (D’Antoni & Veanes POPL’17, cf exercice 1) et décomposition monadique (CAV’14, cf section 6b). La source primaire des trois apports théoriques reliés dans ce notebook.
• RE# (engine F#/.NET, MIT) - github.com/ieviev/resharp-dotnet, NuGet Resharp. &/~ first-class, non-backtracking, temps linéaire (barreau 3).
• Fork Automata (net8.0, MyIntelligenceAgency) - github.com/MyIntelligenceAgency/Automata. Modernise AutomataDotNet (gelé ~2020) : son RegexToSMTConverter compile &/~ de surface vers la théorie des chaînes SMT-LIB 2.6 (re.inter/re.comp) que Z3 résout directement - cap du témoin (#6) levé, plus de produit d’automates. Consommé par le notebook 06 de la série Z3.

Connexions dans cette série

• Sudoku-12 Z3 C# : le résolveur Z3 explore en profondeur (bit-vectors, optimisations). Ce notebook (13) présente le même Z3 sous l’angle narratif “regex symbolique -> SMT -> témoin”.
• Epic #1206 (Z3.Linq DSL) : un autre “geste” de l’auteur (2018), étendre un front-end déclaratif pour laisser Z3 témoigner. La compilation regex -> SMT et le DSL Z3.Linq sont le même geste dans deux librairies.
• Notebook 10 - Générer un témoin depuis A & ~B : le fork Automata levé le cap du témoin (#6) et généralise A & ~B (mots de passe, entrées de test) - le cas où la théorie des chaînes de Z3 est rapide. La section 6b ci-dessus mesure le spectre (rapide en général, lent sur une ligne, unknown à 81).
• Epic #2162 (Game of Life, Lean) : John Conway, à ne pas confondre avec Damian (regex).

La preuve Lean derrière RE

• ezhuchko/finiteness-derivatives (Lean 4, sans Mathlib) : formalise la finitude des dérivées symboliques = le théorème de terminaison/décidabilité derrière la reconnaissance non-backtracking temps linéaire de RE#. Companion CPP 2024 (Zhuchko / Veanes / Ebner).

---

A retenir

• Reconnaître != résoudre : RE# vérifie (temps linéaire), Z3 produit (le témoin). Le Sudoku a besoin des deux.
• Les deux murs de 2020 (explosion DFA, cap témoin ~21 char) étaient des murs de l’automate : ils tombent ensemble dès qu’on change de moteur (&/~ -> théorie des chaînes Z3).
• La dernière marche, le 9x9, se franchit par la forme d’émission du même & d’appartenances : fondu en re.inter il sature (unknown) ; éclaté en la primitive native str.contains (= .*d.* par chiffre) il atterrit la grille 9x9 complète (~53 s en .NET, ~12 s z3-py) - 0 inégalité, le regex se suffit à lui-même.
• Les inégalités 2 à 2 (~0,8 s) et Distinct sur 81 entiers (~38 ms) atterrissent plus vite encore - mais elles quittent le regex. Question de forme d’émission, pas de mur ni de substrat.
• L’ironie : le vérificateur le plus élégant (RE#) certifie, plus vite que Z3 n’a résolu, une grille qu’il ne peut pas produire.