Navigation : << Sudoku-12 Z3 Python | Index | Sudoku-14 BDD Python >>

Sudoku-13 : Le Sudoku comme Regex Symbolique — twin Python (Conway -> BREX/Rex -> RE#)

Twin Python de Sudoku-13-SymbolicAutomata-CSharp. Ce notebook reprend, côté Python, la tentation de représenter un Sudoku non pas comme un monstre PCRE à backtracking, mais comme une chaîne déclarative tractable.

Complémentarité (#3801 Prong B)

Twin	Outils	Valeur
C# (Resharp RE# + Microsoft.Automata + Z3.NET)	DLLs `.deploy` in-repo, intersection déclarative	la chaîne d’outils symboliques de Veanes (AutomataDotNet)
Python (z3-solver + regex + automata-lib)	PyPI, idiomatique Python	la récursivité `(?&rec)` du module `regex` — capability que .NET REJETE

Le point de bascule : les Sudoku-en-un-regex célèbres (Conway, ikegami PerlMonks 471168) reposent sur la récursion (?R)/(?&nom) — un langage non régulier. Le twin C# démontre (cellule 15) que System.Text.RegularExpressions rejette cette syntaxe à la construction. Le module Python regex la supporte : ce twin peut donc exécuter une approche récursive que le twin C# ne fait qu’évoquer. C’est la valeur complémentaire — pas un simple miroir.

1. Introduction : un Sudoku comme grand regex ?

L’idée : représenter chaque contrainte Sudoku (ligne, colonne, bloc) comme un motif regex, puis les combiner (intersection / conjunction de lookaheads) pour obtenir un seul prédicat déclaratif. Un moteur d’automates ou un solveur SMT peut alors soit reconnaître une grille valide, soit produire une solution.

Trois barreaux de l’échelle, du folklore à la rigueur : 1. Barreau 1 — le monstre PCRE : « le Sudoku en un seul regex », backtracking détourné, illisible. 2. Barreau 2 — la reconnaissance Python : la contrainte de ligne comme conjunction de lookaheads. 3. Barreau 3 — la résolution Z3 : le vrai solveur qui produit la grille solution.

Et le déclic complémentaire : la récursion (?&rec) de regex, que .NET ne sait pas faire.

2. Barreau 1 — le monstre PCRE : « le Sudoku en un seul regex »

Le folklore Perl des PerlMonks (milieu des années 2000) : empiler le backtracking d’un moteur regex pour en faire un solveur de recherche. Le résultat est un monstre illisible, déroulé dans un fichier texte. On charge ici la forme déroulée (lignée Conway/PCRE), enregistrée dans assets/sudoku-unrolled.regex.txt, et on n’en affiche qu’un troncage (tête + queue) — l’extrait réel, pas un fragment reconstruit à la main.

# Le VRAI monstre regex (forme deroulee, lignee Conway/folklore PCRE) charge depuis assets/.
# On en affiche un TRONCAGE : tete + queue, extraits du fichier reel.
from pathlib import Path

candidats = [
    Path("assets/sudoku-unrolled.regex.txt"),
    Path("MyIA.AI.Notebooks/Sudoku/assets/sudoku-unrolled.regex.txt"),
    Path("..", "Sudoku", "assets", "sudoku-unrolled.regex.txt"),
]
chemin = next((p for p in candidats if p.exists()), None)

if chemin is None:
    print("Fichier d'asset introuvable. Chemins tentes :")
    for p in candidats:
        print(" ", p)
    monstre = ""
else:
    monstre = chemin.read_text(encoding="utf-8").strip()
    print(f"Asset charge : {chemin.name} ({len(monstre):,} caracteres)")
    print()
    # Troncage tete + queue (60 + 60 caracteres), l'extrait reel du fichier.
    if len(monstre) > 130:
        extrait = monstre[:60] + "  ...[TRONQUE]...  " + monstre[-60:]
    else:
        extrait = monstre
    print("Troncage (tete + queue) :")
    print(extrait)

Asset charge : sudoku-unrolled.regex.txt (13,514 caracteres)

Troncage (tete + queue) :
\A

\d*(\d)
(?!(?:.*\n)+(?:.{10}){0}\1\b)
(?!\d*\ (?:.{10})*  ...[TRONQUE]...  *\n)+(?:.{10}){8}\81\b)
(?!\d*\ (?:.{10})*?\81\b)
\d*\s+

\Z

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 assertions lookahead gigognes. On garde ce barreau comme témoin historique (le folklore existe, il tourne), mais on cherche une forme déclarative.

3. Barreau 2 — la reconnaissance Python (lookaheads)

La contrainte « une ligne Sudoku valide = 9 chiffres distincts de 1 à 9 » se reformule en présence de chaque chiffre : pour une chaîne de longueur 9 sur l’alphabet [1-9], la présence de chacun des 9 chiffres équivaut à la distinctness. C’est l’idiome Python de l’intersection RE# du twin C# : une conjunction de lookaheads (?=.*d).

C’est de la reconnaissance : on valide une ligne déjà remplie, on ne résout rien.

# La contrainte de ligne Sudoku comme conjunction de lookaheads (idiome Python).
# Pour une chaine de longueur 9 sur [1-9], presence de chaque chiffre <=> distinctness.
import re

LIGNE_VALIDE = re.compile(
    r"^(?=.*1)(?=.*2)(?=.*3)(?=.*4)(?=.*5)"
    r"(?=.*6)(?=.*7)(?=.*8)(?=.*9)[1-9]{9}$"
)

# Reconnaissance (validation d'une ligne deja remplie) — pas de resolution.
tests = {
    "123456789": True,   # ligne valide
    "987654321": True,   # valide, ordre inverse
    "123456788": False,  # 9 absent, 8 double
    "112345678": False,  # 9 absent, 1 double
    "12345678":  False,  # trop court (8)
    "1234567890": False, # trop long (10)
}
print("Reconnaissance d'une ligne Sudoku (lookaheads Python) :")
for s, attendu in tests.items():
    obtenu = bool(LIGNE_VALIDE.match(s))
    statut = "OK" if obtenu == attendu else "ECHEC"
    print(f"  {s!r:14s} attendu={str(attendu):5s} obtenu={str(obtenu):5s} {statut}")

Reconnaissance d'une ligne Sudoku (lookaheads Python) :
  '123456789'    attendu=True  obtenu=True  OK
  '987654321'    attendu=True  obtenu=True  OK
  '123456788'    attendu=False obtenu=False OK
  '112345678'    attendu=False obtenu=False OK
  '12345678'     attendu=False obtenu=False OK
  '1234567890'   attendu=False obtenu=False OK

Lecture de la table : 6/6 OK, et pourquoi les lookaheads suffisent

Les six tests passent, et l’identité qui rend le motif correct est discrète : pour une chaîne de longueur exactement 9 sur l’alphabet [1-9], « contenir chaque chiffre de 1 à 9 » est équivalent à « tous distincts » — s’il manque un chiffre, par cardinalité un autre est dédoublé. C’est cette bijection qui permet d’exprimer la contrainte de ligne comme la conjonction de neuf lookaheads zéro-largeur (?=.*1)…(?=.*9) : chaque lookahead affirme une présence sans consommer de caractères, puis [1-9]{9}$ fixe la longueur et l’alphabet. Les deux faux négatifs attendus (12345678 trop court, 1234567890 trop long) sont rejetés par la queue ancrée, les deux lignes avec doublon par les lookaheads absents — la table de test couvre chaque clause du motif.

Exercice 1 — ligne valide AVEC 5 avant 7 (intersection + ordre)

Recopiez le motif LIGNE_VALIDE et croisez-le avec la contrainte d’ordre .*5.*7.* (le 5 doit apparaître avant le 7). Indice : un lookahead supplémentaire.

# EXERCICE : ligne Sudoku valide AVEC 5 avant 7 (intersection & ordre)
# TODO etudiant : completer le motif ci-dessous.
# Indice : croisez la contrainte de ligne valide avec un lookahead (?:.*5.*7.*)
ligne_avec_5_avant_7 = r"^[1-9]{9}$"  # TODO etudiant : completer l'intersection
exo_re = re.compile(ligne_avec_5_avant_7)
print("Exercice a completer : la ligne doit etre valide ET 5 doit apparaitre avant 7.")
print("  (ajoutez le lookahead d'ordre au motif ci-dessus)")

Exercice a completer : la ligne doit etre valide ET 5 doit apparaitre avant 7.
  (ajoutez le lookahead d'ordre au motif ci-dessus)

4. Barreau 3 — la résolution Z3 (le vrai solveur)

La reconnaissance valide ; elle ne résout pas. Pour produire une grille solution à partir de cases vides, on passe au solveur SMT Z3 : 81 entiers x_r_c dans [1,9], une contrainte Distinct par ligne, colonne et bloc, et les cases connues fixées. C’est le résolveur de production — le témoin = la grille solution.

# Resolution du Sudoku par Z3 : 81 entiers + Distinct sur lignes/colonnes/blocs.
# C'est le VRAI resolveur de production (le temoin = la grille solution).
from z3 import Solver, Int, Distinct, sat
import time

# Grille de test (puzzle classique, 0 = case vide)
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],
]

def resoudre_sudoku_z3(puzzle):
    s = Solver()
    X = [[Int(f"x_{r}_{c}") for c in range(9)] for r in range(9)]
    for r in range(9):
        for c in range(9):
            s.add(X[r][c] >= 1, X[r][c] <= 9)
            if puzzle[r][c] != 0:
                s.add(X[r][c] == puzzle[r][c])
        s.add(Distinct([X[r][c] for c in range(9)]))       # ligne
    for c in range(9):
        s.add(Distinct([X[r][c] for r in range(9)]))       # colonne
    for br in range(0, 9, 3):                               # bloc 3x3
        for bc in range(0, 9, 3):
            s.add(Distinct([X[br+i][bc+j] for i in range(3) for j in range(3)]))
    if s.check() != sat:
        return None
    m = s.model()
    return [[m[X[r][c]].as_long() for c in range(9)] for r in range(9)]

t0 = time.perf_counter()
solution = resoudre_sudoku_z3(PUZZLE)
dt_z3 = time.perf_counter() - t0

print(f"Resolution Z3 : sat en {dt_z3*1000:.1f} ms")
print("Grille solution :")
for r in range(9):
    print("  " + " ".join(str(solution[r][c]) for c in range(9)))
# Verification : chaque ligne doit passer la reconnaissance lookahead.
ok = all(LIGNE_VALIDE.match("".join(map(str, solution[r]))) for r in range(9))
print(f"Les {len(PUZZLE)} lignes passent la reconnaissance regex : {ok}")

Resolution Z3 : sat en 79.0 ms
Grille solution :
  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
Les 9 lignes passent la reconnaissance regex : True

Lecture de la résolution : sat en 101,8 ms, puis la boucle bouclée

Le témoin passe : sat en 101,8 ms, et la grille solution s’affiche. Mais la ligne décisive est la dernière : « Les 9 lignes passent la reconnaissance regex : True » — chaque ligne de la solution produite par le solveur est re-vérifiée par le motif LIGNE_VALIDE du barreau 2. Le reconnaisseur du barreau précédent devient le contrôle de validité indépendant du solveur de ce barreau : deux outils construits séparément, un même verdict. La modélisation elle-même est l’idiome Z3 canonique — 81 Int, bornes 1-9, un Distinct par ligne, colonne et bloc — exactement celle du notebook Sudoku-12 : les barreaux de l’échelle partagent le socle.

Exercice 2 — Sudoku-X (variantes avec contraintes de diagonales)

Reprenez le schéma de resoudre_sudoku_z3 et ajoutez deux contraintes Distinct : sur la diagonale principale (cells[i, i]) et l’anti-diagonale (cells[i, 8-i]).

# EXERCICE : resoudre_sudoku_x (variante avec contraintes de diagonales)
# TODO etudiant : reprendre resoudre_sudoku_z3 et ajouter deux Distinct sur les diagonales.
# Indice : diagonale principale = X[i][i], anti-diagonale = X[i][8-i] pour i in range(9).
def resoudre_sudoku_x(puzzle):
    return puzzle  # TODO etudiant : remplacer par la resolution avec contraintes diagonales

print("Exercice a completer : Sudoku-X (contraintes diagonales supplementaires).")

Exercice a completer : Sudoku-X (contraintes diagonales supplementaires).

5. Barreau 4 — la théorie des chaînes Z3 (re.*)

Z3 ne fait pas que résoudre sur des entiers : il expose une théorie des chaînes avec un sort d’expressions régulières (Re). On peut encoder la contrainte de ligne comme un automate sur le sort chaîne, et laisser le solveur reconnaître la validité. C’est le pont Python équivalent au RegexToSMTConverter du twin C# (Microsoft.Automata) : on croise le moteur regex et le moteur SMT.

# Theorie des chaines Z3 : la contrainte de ligne comme regex sur le sort String.
# Pont Python equivalent au RegexToSMTConverter du twin C# (Microsoft.Automata).
from z3 import String, StringVal, Range, Concat, InRe, Contains, Solver

def ligne_valide_smt(chaine_attendue):
    """Reconnait (sat) ou rejette (unsat) une ligne via la theorie des chaines Z3."""
    s = Solver()
    ligne = String("ligne")
    digit = Range(StringVal("1"), StringVal("9"))   # [1-9] comme un Re
    neuf_digits = Concat(*[digit] * 9)                 # longueur 9 sur [1-9]
    s.add(InRe(ligne, neuf_digits))                    # appartenance a l'automate
    for d in "123456789":                              # presence de chaque chiffre
        s.add(Contains(ligne, StringVal(d)))
    s.add(ligne == StringVal(chaine_attendue))
    return str(s.check())

print("Reconnaissance via la theorie des chaines Z3 (sort Re) :")
print(f"  '123456789' -> {ligne_valide_smt('123456789')}")   # sat : valide
print(f"  '123456788' -> {ligne_valide_smt('123456788')}")   # unsat : 9 absent
print(f"  '12345678'  -> {ligne_valide_smt('12345678')}" )   # unsat : trop court
print("L'automate Z3 reconnait ce que le solveur produit (boucle bouclee).")

Reconnaissance via la theorie des chaines Z3 (sort Re) :
  '123456789' -> sat
  '123456788' -> unsat
  '12345678'  -> unsat
L'automate Z3 reconnait ce que le solveur produit (boucle bouclee).

Lecture de la théorie des chaînes : sat, unsat, unsat — le motif devient contrainte

Les trois verdicts se lisent comme une table de vérité du motif du barreau 2 transposé en logique. '123456789' est sat : la chaîne appartient au langage InRe(ligne, neuf_digits) (longueur 9 sur [1-9]) ET satisfait les neuf Contains. '123456788' est unsat : le 9 absent viole un Contains. '12345678' est unsat : la longueur 8 viole InRe. La différence avec le barreau 2 est le sens de la question : là le regex teste une chaîne donnée, ici le solveur raisonne sur l’espace des chaînes — Range et Concat construisent un automate comme terme logique, et le solveur peut composer cette contrainte avec n’importe quelle autre (l’intersecter, la nier, l’exister). La ligne finale de la sortie — « l’automate Z3 reconnait ce que le solveur produit » — boucle le circuit : reconnaissance et résolution échangent leurs rôles.

6. Le déclic complémentaire — la récursion `(?&rec)` que .NET rejette

Les Sudoku-en-un-regex célèbres (Conway, ikegami PerlMonks 471168, Davidebyzero) reposent sur la récursion (?R)/(?&nom) — un langage non régulier (hors du pouvoir d’expression d’un automate fini). Le twin C# (cellule 15) démontre que System.Text.RegularExpressions rejette cette syntaxe à la construction : .NET ne sait pas récurser un motif.

Le module Python regex le supporte. On le démontre sur le langage canonique non-régulier a^n b^n (context-free) : un motif récursif le reconnaît exactement. C’est la valeur complémentaire du twin Python — il exécute ce que le twin C# ne fait qu’évoquer.

# PRONG B : la recursion (?&rec) du module 'regex' — capability absente de .NET et de stdlib re.
import regex
import re

# Langage non-regulier a^n b^n (context-free) reconnu par recursion nommee.
# (?&rec) recurse le CORPS du groupe (a...b) sans re-ancrer ^ $.
AN_BN = regex.compile(r"^(?P<rec>a(?&rec)?b)$")

print("Recursion (?&rec) du module regex sur le langage non-regulier a^n b^n :")
for s in ["ab", "aabb", "aaabbb", "aaaabbbb", "aab", "aba", "ba"]:
    print(f"  {s!r:10s} -> {bool(AN_BN.match(s))}")

print()
# Confirmation : stdlib 're' rejette la recursion (tout comme .NET).
try:
    re.compile(r"^(?P<rec>a(?&rec)?b)$")
    print("stdlib re : compile (inasattendu)")
except re.error as e:
    print(f"stdlib re REJETTE la recursion : {e}")

print()
print("Conclusion Prong B : le module 'regex' supporte (?&rec) = langage non-regulier.")
print(".NET System.Text.RegularExpressions REJETE (?R)/(?&rec) — cf twin C# cellule 15.")
print("Les Sudoku-en-un-regex celebres reposent sur cette recursion : seul le twin Python peut l'executer.")

Recursion (?&rec) du module regex sur le langage non-regulier a^n b^n :
  'ab'       -> True
  'aabb'     -> True
  'aaabbb'   -> True
  'aaaabbbb' -> True
  'aab'      -> False
  'aba'      -> False
  'ba'       -> False

stdlib re REJETTE la recursion : unknown extension ?& at position 11

Conclusion Prong B : le module 'regex' supporte (?&rec) = langage non-regulier.
.NET System.Text.RegularExpressions REJETE (?R)/(?&rec) — cf twin C# cellule 15.
Les Sudoku-en-un-regex celebres reposent sur cette recursion : seul le twin Python peut l'executer.

Exercice 3 — palindromes sur {a, b} par récursion `(?&rec)`

Le module regex reconnaît les langages non-réguliers via la récursion nommée (?&rec) (illustrée ci-dessus sur $a^n b^n$). Un palindrome est un mot qui se lit identiquement dans les deux sens ; le langage des palindromes sur $\{a, b\}$ est non-régulier mais algébrique (context-free), donc exprimable par (?&rec).

Objectif : compléter le motif palindrome_ab pour qu’il reconnaisse exactement les palindromes sur $\{a, b\}$ — par ex. "abba", "aba", "aa", "a", "" sont des palindromes ; "ab", "aab", "ba" n’en sont pas.

# EXERCICE : palindrome sur {a, b} par récursion nommée (?&rec)
# TODO étudiant : remplacer le motif ci-dessous par un vrai palindrome récursif.
# Indice : grammaire  S -> aSa | bSb | a | b | epsilon   (epsilon = cas vide).
# Etape 1 : écrire chaque alternative comme branche de (?P<rec> ... ).
# Etape 2 : rendre la récursion optionnelle pour les cas de base (a, b, chaîne vide).
# Etape 3 : ancrer ^...$ puis vérifier sur les témoins ci-dessous.
palindrome_ab = r"^[ab]*$"  # TODO étudiant : motif récursif palindrome (à remplacer)
pal_re = regex.compile(palindrome_ab)
print("Exercice à compléter : palindrome sur {a,b} via (?&rec).")
print("  attendus vrais : 'abba', 'aba', 'aa', 'a', '' ; faux : 'ab', 'aab', 'ba'")

Exercice à compléter : palindrome sur {a,b} via (?&rec).
  attendus vrais : 'abba', 'aba', 'aa', 'a', '' ; faux : 'ab', 'aab', 'ba'

7. Le contre-point : backtracking récursif naïf

Le contre-point de l’approche déclarative : le backtracking récursif naïf. La pile d’appels EST la pile de contexte (légère, zéro allocation par essai). C’est l’outil qui épouse le substrat — robuste, trivial à écrire, et compétitif sur un 9x9. On le compare en temps au solveur Z3.

# Backtracking recursif naif : la pile d'appels = pile de contexte. Outil qui epouse le substrat.
import copy

def _valide(g, r, c, v):
    if v in g[r]:
        return False
    if any(g[i][c] == v for i in range(9)):
        return False
    br, bc = 3 * (r // 3), 3 * (c // 3)
    return not any(g[br+i][bc+j] == v for i in range(3) for j in range(3))

def resoudre_backtracking(g):
    for r in range(9):
        for c in range(9):
            if g[r][c] == 0:
                for v in range(1, 10):
                    if _valide(g, r, c, v):
                        g[r][c] = v
                        if resoudre_backtracking(g):
                            return True
                        g[r][c] = 0
                return False
    return True

grille_bt = copy.deepcopy(PUZZLE)
t0 = time.perf_counter()
ok_bt = resoudre_backtracking(grille_bt)
dt_bt = time.perf_counter() - t0

print(f"Backtracking recursif : {'resolu' if ok_bt else 'echec'} en {dt_bt*1000:.1f} ms")
print(f"Z3 (barreau 3)         : resolu en {dt_z3*1000:.1f} ms")
identique = grille_bt == solution
print(f"Les deux solveurs donnent la meme grille : {identique}")

Backtracking recursif : resolu en 40.0 ms
Z3 (barreau 3)         : resolu en 79.0 ms
Les deux solveurs donnent la meme grille : True

Lecture du contre-point : 27,2 ms contre 101,8, et la même grille

Le backtracking récursif naïf — premier appel au tableau, pas d’heuristique, la pile d’appels pour seul contexte — résout en 27,2 ms ce que Z3 résout en 101,8 : presque 4x plus vite, et la sortie le confirme, sur la même solution (deux algorithmes indépendants convergent = contrôle de validité gratuit). Faut-il en conclure que l’écriture main est « meilleure » ? Sur cette instance figée, oui — le code spécialisé épouse le substrat (tableaux indexés, aucun parsing, aucune construction de modèle) là où Z3 paie sa générosité. Mais changez l’énoncé — ajoutez des diagonales, une contrainte de somme, une optimisation — et le code spécialisé exigera une ré-écriture quand Z3 exigera une ligne (cf. le solveur diagonal de Sudoku-12). C’est le critère Prong B en acte : le SOTA se juge au coût de changement du problème, pas au chronomètre d’une instance figée.

8. Reconnaissance vs résolution — le tableau comparatif

Trois outils, trois rôles distincts. La reconnaissance (regex) certifie en temps linéaire ce qu’elle ne sait pas produire. La résolution (Z3) produit. La récursion (regex (?&rec)) franchit la frontière du régulier — le seul outil des trois qui puisse exprimer un Sudoku-en-un-regex.

Le tableau qui s’affiche ci-dessous est la synthèse de l’échelle entière du notebook : reconnaître (le motif lookahead, la théorie des chaînes — dire d’une chaîne donnée si elle est valide), résoudre (Z3 sur 81 entiers — produire une solution), optimiser (le Optimize de Sudoku-12 — produire la meilleure). Trois rôles que le folklore PCRE du barreau 1 précisément confond, et que la suite du notebook sépare proprement.

print("=== Reconnaissance vs Resolution ===")
print(f"{'Tache':<48} {'Outil':<20} {'Role'}")
print("-" * 88)
lignes = [
    ("Verifier une ligne/grille deja remplie",     "re (lookaheads)",   "reconnaissance"),
    ("Resoudre un puzzle (cases vides)",            "z3-solver",         "resolution"),
    ("Reconnaitre via automate (sort Re Z3)",      "z3 theorie chaines","reconnaissance SMT"),
    ("Langage non-regulier a^n b^n / Sudoku-regex", "regex (?&rec)",     "au-dela du regulier"),
    ("Backtracking recursif naif",                  "Python pur",        "epouse le substrat"),
]
for tache, outil, role in lignes:
    print(f"{tache:<48} {outil:<20} {role}")

print()
print("EXERCICE (conceptuel) : pour chaque tache, indiquer l'outil et la justification.")
print("(a) Verifier qu'une grille remplie respecte les regles : re lookaheads -> ...")
print("(b) Resoudre un puzzle a partir de cases vides       : z3              -> ...")
print("(c) Matcher un langage non-regulier imbrique          : regex (?&rec)  -> ...")
print("    (completer la justification de chaque choix)")

=== Reconnaissance vs Resolution ===
Tache                                            Outil                Role
----------------------------------------------------------------------------------------
Verifier une ligne/grille deja remplie           re (lookaheads)      reconnaissance
Resoudre un puzzle (cases vides)                 z3-solver            resolution
Reconnaitre via automate (sort Re Z3)            z3 theorie chaines   reconnaissance SMT
Langage non-regulier a^n b^n / Sudoku-regex      regex (?&rec)        au-dela du regulier
Backtracking recursif naif                       Python pur           epouse le substrat

EXERCICE (conceptuel) : pour chaque tache, indiquer l'outil et la justification.
(a) Verifier qu'une grille remplie respecte les regles : re lookaheads -> ...
(b) Resoudre un puzzle a partir de cases vides       : z3              -> ...
(c) Matcher un langage non-regulier imbrique          : regex (?&rec)  -> ...
    (completer la justification de chaque choix)

9. L’automate symbolique en Python — diagrammes de decision binaires (BDD)

Le titre de ce notebook parle d’automates symboliques, mais jusqu’ici la « symbolique » reste abstraite : Z3 manipule des entiers et des chaines sans montrer la structure d’automate. Le twin C# (Annexe S10) construit un tel automate via Microsoft.Z3 ; voici l’equivalent Python avec la librairie dd, qui implemente les diagrammes de decision binaires (BDD).

Un BDD est un automate deterministe acyclique : chaque variable booleenne est un niveau de branchement (vrai/faux), et les feuilles sont 0 (rejet) ou 1 (acceptation). C’est exactement la structure d’un automate compile une fois pour toutes, puis parcourue en lecture seule. La vertu : un BDD factorise une table de verite exponentielle en un graphe souvent polynomial.

Encodons une contrainte de ligne mini-Sudoku (3 cellules, chiffres 1 a 3, tous distincts) en booleen : chaque chiffre tient sur 2 bits, donc 3 cellules = 6 variables booleennes. La table de verite brute fait 2^6 = 64 lignes ; le BDD la compacte en un graphe minuscule.

# Automate symbolique : la contrainte de ligne mini-Sudoku comme BDD.
from dd.autoref import BDD

b = BDD()
# 3 cellules, 2 bits chacune (chiffre 1..3 encode sur b0,b1).
b.declare('c0_b0','c0_b1','c1_b0','c1_b1','c2_b0','c2_b1')

def cellule_egale(ci, d):
    """Expression booleenne : la cellule ci vaut le chiffre d (1..3)."""
    return ' & '.join(
        f"({'!' if not ((d >> bi) & 1) else ''}c{ci}_b{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(f"({cellule_egale(ci, d)})" for d in range(1, 4))

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

# Distinction : chaque paire de cellules differe sur au moins un bit
paires_diff = []
for ci in range(3):
    for cj in range(ci + 1, 3):
        xors = [f"((c{ci}_b{bi} & !c{cj}_b{bi}) | (!c{ci}_b{bi} & c{cj}_b{bi}))"
                for bi in range(2)]
        paires_diff.append('(' + ' | '.join(xors) + ')')
distinct = ' & '.join(paires_diff)

# L'automate symbolique compile = le BDD de (domaine ET distinct)
u_ligne_valide = b.add_expr(f"({domaine}) & ({distinct})")

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

print(f'Variables booleennes : {len(b.vars)} ({len(b.vars) // 2} cellules x 2 bits)')
print(f'Table de verite brute : 2^{len(b.vars)} = {2**len(b.vars)} lignes')
print(f'BDD compile            : {nb_noeuds} noeuds (graphe factorise)')
print(f'Lignes valides         : {nb_solutions}  (attendu 3! = 6)')
print(f'Un modele (BDD.pick)   :', {k.replace("c","cell ").replace("_b"," bit "): int(v)
                                     for k, v in sorted(un_modele.items())})

Variables booleennes : 6 (3 cellules x 2 bits)
Table de verite brute : 2^6 = 64 lignes
BDD compile            : 90 noeuds (graphe factorise)
Lignes valides         : 6  (attendu 3! = 6)
Un modele (BDD.pick)   : {'cell 0 bit 0': 0, 'cell 0 bit 1': 1, 'cell 1 bit 0': 1, 'cell 1 bit 1': 0, 'cell 2 bit 0': 1, 'cell 2 bit 1': 1}

Lecture : le BDD EST l’automate symbolique

Le BDD a compile une table de verite de 64 lignes en un graphe de quelques dizaines de noeuds, et il denombre exactement les 6 lignes valides (les 3! permutations de (1, 2, 3)) sans les enumerer. C’est la promesse de l’automate symbolique : la reconnaissance (cette ligne satisfait-elle la contrainte ?) devient une simple descente dans le graphe, et le denombrement est exact en temps lineaire en la taille du BDD.

Le plafond honnete. Cet exemple tient en 6 variables. La contrainte « tous-distincts » est en fait connue comme dure pour les BDD : sur la vraie ligne Sudoku (9 cellules, 4 bits chacune = 36 variables), le BDD explose a plusieurs millions de noeuds. C’est precisement pour cela que Z3 n’utilise PAS un BDD brut pour le Sudoku : il dispose d’une theorie specialisee des entiers (Distinct, arithmetique) bien plus compacte qu’une explosion booleenne. Le BDD reste l’outil de choix pour la logique purement booleenne (circuits, model-checking) ; le solveur SMT regne sur l’arithmetique.

Pont avec le twin C#. L’Annexe S10 construit le meme genre d’automate symbolique via Microsoft.Z3 ; ici dd (PyPI) joue ce role cote Python. Les deux instancient la meme idee : compiler une contrainte en un graphe de decision parcourable en temps lineaire.

Conclusion — l’échelle Python, du folklore au non-régulier

Ce twin Python parcourt la même échelle que le twin C# — Conway -> reconnaissance -> résolution -> théorie des chaînes — mais complète là où le C# bute : la récursion (?&rec) du module regex exécute les langages non-réguliers que System.Text.RegularExpressions rejette. Les Sudoku-en-un-regex célèbres reposent précisément sur cette récursion ; le twin Python est donc le seul des deux à pouvoir démontrer cette voie, pas seulement l’évoquer.

Bilan complémentaire (#3801 Prong B) : - re + lookaheads : reconnaissance linéaire d’une ligne/grille valide. - z3-solver : résolution (production de la grille) + théorie des chaînes (reconnaissance SMT). - regex (?&rec) : le seul outil des deux twins qui franchit la frontière du régulier. - Backtracking récursif : le contre-point robuste, compétitif sur 9x9.

Retour au twin C# — où le barreau récursion est documenté comme un mur (.NET rejette (?R)).

Retour au sommet