Jusqu’ici, chaque variable Z3 vivait seule (Int("x"), Int("y")). Beaucoup de problèmes combinatoires — Sudoku, carrés magiques, planification sur grille — raisonnent sur un tableau 2D. Z3 offre deux encodages canoniques d’une telle grille, que ce notebook compare :
L’encodage déclaratif (idiomatique z3-py). Une grille n × n devient une liste de listes de variables Int, une par case. Les contraintes (Distinct par ligne, par colonne, par bloc) s’écrivent en Python natif, avec des compréhensions. C’est l’analogue direct du Theorem<Grid> du binding C# Z3.Linq, sans la couche DSL.
L’encodage brut (théorie des tableaux SMT). La grille est un ArraydeArray (Int → (Int → Int)) manipulé par Store / Select. Plus verbeux, mais c’est la vraie théorie des tableaux de McCarthy, exposée par z3-py sans intermédiaire.
L’objectif est de montrer comment le même changement de paradigme (décrire les contraintes, laisser le solveur trouver la solution) s’étend du scalaire à la grille, et comment z3-py donne accès aux deux niveaux : l’élégance déclarative pour la pédagogie, et l’API brute pour comprendre ce qui se passe sous le capot.
# Imports : z3 (solveur SMT) + pprint (affichage lisible des grilles).from z3 import (Solver, Int, Distinct, Sum, And, Or, sat, ArraySort, IntSort, K, IntVal, Store, Select)from pprint import pprint# z3-py est monocanal ; on neutralise le parallélisme interne pour des exécutions reproductibles.from z3 import set_paramset_param('parallel.enable', False)print("Imports OK : z3 (théorie des tableaux, Optimize), pprint.")
Imports OK : z3 (théorie des tableaux, Optimize), pprint.
1. Carré latin 3×3 — l’approche déclarative
Un carré latinn × n contient les valeurs 1..n, chacune apparaissant une seule fois par ligne et une seule fois par colonne. C’est le squelette nu d’un Sudoku (sans les blocs).
Encodage déclaratif : neuf variables Int, une par case, contraintes par des Distinct par ligne et par colonne. Aucune boucle de backtracking à écrire : on décrit la propriété mathématique de la solution, le solveur la satisfait.
def carre_latin_3(): s = Solver()# Grille 3x3 : une variable Int par case. g = [[Int(f"L_{r}_{c}") for c inrange(3)] for r inrange(3)]# Domaine 1..3 + une valeur unique par ligne et par colonne.for r inrange(3):for c inrange(3): s.add(g[r][c] >=1, g[r][c] <=3) s.add(Distinct(g[r])) # ligne r : toutes différentesfor c inrange(3): s.add(Distinct([g[r][c] for r inrange(3)])) # colonne c : toutes différentesassert s.check() == sat m = s.model()return [[m[g[r][c]].as_long() for c inrange(3)] for r inrange(3)]print("Carré latin 3x3 :")pprint(carre_latin_3())
Interprétation 1 — le pattern « compréhension + Distinct »
Le corps de la contrainte tient en deux boucles : une pour les lignes, une pour les colonnes. Chaque Distinct([...]) est l’encodage direct de « toutes différentes ». Notez qu’aucune heuristic d’énumération n’apparaît : Z3 raisonne sur les neuf variables simultanément et produit une affectation cohérente. C’est le saut de paradigme — on ne programme pas la recherche, on déclare la structure.
2. Sudoku 4×4 — le cas d’usage canonique
Le Sudoku ajoute aux contraintes du carré latin une contrainte de bloc : la grille 4×4 se découpe en quatre blocs 2×2, chacun devant contenir 1..4 sans répétition.
On résout deux instances : la grille vide (le solveur trouve une solution parmi les 960 grilles 4×4 valides) puis une grille avec givens (indices imposés). La seule différence d’encodage est l’ajout de g[r][c] == v pour chaque donné.
def sudoku_4x4(givens=None): givens = givens or {} s = Solver() g = [[Int(f"S_{r}_{c}") for c inrange(4)] for r inrange(4)]# Domaine 1..4.for r inrange(4):for c inrange(4): s.add(g[r][c] >=1, g[r][c] <=4) s.add(Distinct(g[r])) # lignefor c inrange(4): s.add(Distinct([g[r][c] for r inrange(4)])) # colonne# Blocs 2x2.for br inrange(0, 4, 2):for bc inrange(0, 4, 2): bloc = [g[br + i][bc + j] for i inrange(2) for j inrange(2)] s.add(Distinct(bloc))# Givens (indices imposés).for (r, c), v in givens.items(): s.add(g[r][c] == v)assert s.check() == sat m = s.model()return [[m[g[r][c]].as_long() for c inrange(4)] for r inrange(4)]print("Sudoku 4x4 (grille vide) :")pprint(sudoku_4x4())givens = {(0, 0): 1, (1, 3): 2, (2, 1): 3, (3, 2): 4}print(f"\nSudoku 4x4 avec givens {dict(sorted(givens.items()))} :")pprint(sudoku_4x4(givens))
Interprétation 2 — la grille 2D comme liste de listes
L’encodage g = [[Int(...) for c ...] for r ...] est lisible et se prête à toute transformation Python (extraction d’un bloc par slicing de comprehension, ajout d’un donné par affectation d’égalité). Le solveur gère la combinatoire sous-jacente — ici 16 variables sur un domaine de 4 valeurs, soit 4^16 ≈ 4 milliards d’affectations brutes que Z3 explore symboliquement sans énumération.
3. Carré magique 3×3 — sommes de lignes et colonnes
Un carré magique d’ordre 3 place les entiers 1..9 (tous distincts) dans une grille 3×3 telle que chaque ligne, chaque colonne et chaque diagonale somment à la constante magiqueM = n(n²+1)/2 = 15. C’est l’exemple historique (le Lo Shu, Chine antique, ~2200 av. J.-C.).
L’encodage ajoute au carré latin une contrainte de somme (Sum(...) == 15) sur chaque ligne, colonne et diagonale. La contrainte Distinct sur les neuf cases garantit l’usage exact des entiers 1..9.
def carre_magique_3(): s = Solver() g = [[Int(f"M_{r}_{c}") for c inrange(3)] for r inrange(3)] plat = [g[r][c] for r inrange(3) for c inrange(3)]for v in plat: s.add(v >=1, v <=9) s.add(Distinct(plat)) # 9 valeurs toutes différentes MAGIE =15for r inrange(3): s.add(Sum(g[r]) == MAGIE) # somme de chaque lignefor c inrange(3): s.add(Sum([g[r][c] for r inrange(3)]) == MAGIE) # somme de chaque colonne s.add(Sum([g[i][i] for i inrange(3)]) == MAGIE) # diagonale principale s.add(Sum([g[i][2- i] for i inrange(3)]) == MAGIE) # diagonale opposéeassert s.check() == sat m = s.model()return [[m[g[r][c]].as_long() for c inrange(3)] for r inrange(3)]sol = carre_magique_3()print("Carré magique 3x3 (constante = 15) :")pprint(sol)# Vérification : la solution satisfait bien toutes les contraintes de somme.print("Sommes lignes :", [sum(sol[r]) for r inrange(3)])print("Sommes colonnes :", [sum(sol[r][c] for r inrange(3)) for c inrange(3)])
Sum([...]) == 15 est une contrainte linéaire entière que le solveur traite au même titre qu’une inégalité. Le carré magique combine donc trois familles de contraintes — domaine (1..9), toutes différentes (Distinct), somme exacte (Sum) — dans un même solveur. La solution trouvée est le Lo Shu classique (à rotation/symétrie près, puisque le solveur renvoie la première solution sat).
L’encodage déclaratif cache la mécanique : il n’y a pas de « vrai » tableau Z3, seulement des variables scalaires nommées L_0_0, L_0_1… La théorie des tableaux de Z3 (axiomes de McCarthy : select(store(a, i, v), i) == v et select(store(a, i, v), j) == select(a, j) si i != j) offre un véritable tableau symbolique via Array.
Pour une grille 2D, on emboîte deux Array : un tableau externeInt → (Int → Int) qui mappe l’indice de ligne à un tableau interneInt → Int (la ligne). La cellule (i, j) se lit Select(Select(grid, i), j) et s’écrit par Store imbriqué. L’exemple construit une grille 2×2 [[1, 2], [3, 4]] et relit chaque cellule.
def grille_2d_raw(): s = Solver()# Tableau interne constant (tout index -> 0) : K(sort, valeur). zero = K(IntSort(), IntVal(0))# Construction de chaque ligne par Store successifs. ligne0 = Store(Store(zero, 0, 1), 1, 2) # ligne 0 = [1, 2, 0, 0, ...] ligne1 = Store(Store(zero, 0, 3), 1, 4) # ligne 1 = [3, 4, 0, 0, ...]# Grille externe : Int -> (Int -> Int). On stocke chaque ligne à son indice. grille = Store(Store(K(IntSort(), zero), 0, ligne0), 1, ligne1)# Vérification : lecture de chaque cellule par Select imbriqué. s.add(Select(Select(grille, 0), 0) ==1) s.add(Select(Select(grille, 0), 1) ==2) s.add(Select(Select(grille, 1), 0) ==3) s.add(Select(Select(grille, 1), 1) ==4)assert s.check() == sat m = s.model()return [[m.eval(Select(Select(grille, i), j)).as_long() for j inrange(2)] for i inrange(2)]print("Grille 2x2 (Array de Array, Store/Select) :")pprint(grille_2d_raw())
Les deux encodages produisent la même grille, mais ils ne servent pas le même but :
Aspect
Déclaratif (listes de Int)
Brut (Array de Array)
Lisibilité
Python natif, compréhensions
Store/Select emboîtés, verbeux
Sémantique
Variables scalaires liées par contraintes
Vrai tableau symbolique de McCarthy
Cas d’usage
Pédagogie, Sudoku, puzzles
Vérification de programmes, état mutable
Quand l’utiliser
Toujours pour modéliser un puzzle
Dès qu’on raisonne sur un tableau en tant que tel (mise à jour en place, preuve de tri, etc.)
Le brut est l’outil de choix pour la vérification de programmes (prouver qu’un tri modifie un tableau comme attendu) ; le déclaratif est l’outil de choix pour la modélisation de puzzles. z3-py expose les deux sans intermédiaire — là où le binding C# Z3.Linq masque le brut derrière son DSL Theorem<Grid>.
5. Exercices
Les trois exercices suivants étendent les modèles ci-dessus. Chaque stub est à compléter : votre code doit produire une solution vérifiée (le solveur la satisfait par construction).
Exercice 1 — Carré latin 3×3 avec contraintes diagonales
Reprenez le modèle du carré latin 3×3 (cellule §1) et ajoutez la contrainte que les deux diagonales sont aussi « toutes différentes ». Combien de solutions reste-t-il ? Affichez-en une.
Indice : Distinct([g[i][i] for i in range(3)]) et Distinct([g[i][2-i] for i in range(3)]). Pour compter les solutions, ajoutez une contrainte bloquante (s.add(Or(...))) à chaque tour via Solver.block_vars ou en niant le modèle trouvé.
# Exercice 1 : carré latin 3x3 avec diagonales aussi toutes différentes.# TODO étudiant :# Etape 1 : reprendre la grille 3x3 et les contraintes ligne/colonne de la cellule §1.# Etape 2 : ajouter Distinct sur la diagonale principale et la diagonale opposée.# Etape 3 : afficher une solution.## Indice : Distinct([g[i][i] for i in range(3)]) et Distinct([g[i][2-i] for i in range(3)])print("Exercice 1 à compléter : carré latin 3x3 avec contraintes diagonales.")
Exercice 1 à compléter : carré latin 3x3 avec contraintes diagonales.
Exercice 2 — Sudoku 4×4 avec une autre grille de départ
Reprenez sudoku_4x4 et résolvez avec une grille de départ différente et plus contraignante (par exemple 5 givens bien choisis). Vérifiez que la solution respecte tous les givens.
Indice : passez un dictionnaire givens plus fourni à sudoku_4x4, puis assertez que chaque solution renvoyée contient bien la valeur imposée à chaque position donnée.
# Exercice 2 : Sudoku 4x4 avec une grille de départ différente (>= 5 givens).# TODO étudiant :# Etape 1 : choisir 5 givens cohérents (qui n'épuisent aucune ligne/colonne/bloc).# Etape 2 : appeler sudoku_4x4(givens) et afficher la solution.# Etape 3 : vérifier que la solution respecte chaque donné (assert par assert).print("Exercice 2 à compléter : Sudoku 4x4 avec une autre grille de départ.")
Exercice 2 à compléter : Sudoku 4x4 avec une autre grille de départ.
Exercice 3 — Vérificateur de carré magique
Écrivez un vérificateur qui, étant donné une grille 3×3 concrète (par exemple [[2,7,6],[9,5,1],[4,3,8]]), utilise Z3 pour prouver qu’elle est magique (ou exhiber la contrainte violée). On fixe les variables aux valeurs de la grille puis on vérifie que toutes les contraintes de somme (cellule §3) sont satisfaites.
Indice : s.add(g[r][c] == valeur[r][c]) pour figer la grille, puis s.check() == sat prouve que toutes les contraintes de somme tiennent.
# Exercice 3 : vérifier qu'une grille 3x3 concrète est un carré magique.# TODO étudiant :# Etape 1 : figer g[r][c] aux valeurs d'une grille candidate (ex. [[2,7,6],[9,5,1],[4,3,8]]).# Etape 2 : ajouter les contraintes de somme (lignes, colonnes, diagonales = 15).# Etape 3 : s.check() == sat prouve que la grille est magique ; sinon, elle ne l'est pas.print("Exercice 3 à compléter : vérificateur de carré magique.")
Exercice 3 à compléter : vérificateur de carré magique.
Conclusion
Ce notebook a étendu la modélisation Z3 du scalaire à la grille 2D, via deux encodages complémentaires :
Déclaratif (listes de Int + Distinct/Sum) : l’outil de choix pour modéliser puzzles et problèmes combinatoires sur grille — carré latin, Sudoku, carré magique.
Brut (Array de Array, Store/Select) : la théorie des tableaux de McCarthy, indispensable pour raisonner sur un tableau en tant qu’objet mutable (vérification de tri, preuve de programmes).
Le même changement de paradigme — décrire les contraintes, pas l’algorithme — passe du scalaire à la grille sans rupture de style : on ajoute des dimensions aux compréhensions Python, et le solveur gère la combinatoire. C’est précisément ce que rend visible l’API complète de z3-py, sans la couche déclarative du binding C# Z3.Linq.
Pour aller plus loin : combinez l’encodage grille avec Optimize (cellule §6 du notebook 06) pour des variantes optimisées — par exemple le carré magique anti-magique (sommes toutes différentes) ou un Sudoku avec objectif de minimiser le nombre de givens.