Z3-Python 18 — Sudoku 4x4 : comparaison des modes `Array` et `Constants`

Navigation : Index Z3-Python | Index SMT | Index SymbolicAI | Série Z3 C#

Objectifs d’apprentissage

À la fin de ce notebook, vous saurez : 1. Modéliser le même Sudoku 4x4 de deux façons différentes en Z3 — un encodage par Int constants (un par cellule), un encodage par Array (théorie des tableaux). 2. Énoncer les contraintes canoniques du Sudoku 4x4 (domaine 1..4, rangées/colonnes/blocs 2x2 à valeurs distinctes) dans chaque mode. 3. Vérifier que les deux encodages convergent vers une solution valide (carré latin), et comprendre pourquoi le choix d’encodage n’affecte pas la sémantique mais peut affecter la performance.

Ce notebook est le port Python (pyz3) du notebook C# 03_Sudoku_Modes_Comparison. Il complète le notebook Z3-Python-02 Sudoku (qui résout le Sudoku dans un seul mode) en montrant que deux modélisations équivalentes du même problème mènent au même résultat — une leçon clé sur la séparation entre problème (les contraintes) et encodage (comment on les exprime).

# Imports et verification de l'environnement.
# Le package pip s'appelle 'z3-solver' (et non 'z3').
# !pip install z3-solver

from z3 import *

print(f"Imports OK : z3-solver version {get_version_string()}")

Imports OK : z3-solver version 4.16.0

1. Vue d’ensemble — un même Sudoku, deux modes d’encodage

Un Sudoku 4x4 se modélise par 16 cellules prenant des valeurs dans {1, 2, 3, 4}, soumises à trois familles de contraintes : chaque rangée, chaque colonne et chaque bloc 2x2 contient des valeurs distinctes. Z3 permet d’exprimer ces 16 cellules de deux manières fondamentalement différentes :

Mode	Encodage pyz3	Analogie
Constants	16 variables `Int` séparées (`c_0_0`, `c_0_1`, …, `c_3_3`)	un tableau de scalaires
Array	un `Array(Int, Int)` indexé par `r*4+c` (théorie des tableaux)	une fonction Index → Valeur

Les deux modes sont sémantiquement équivalents : ils expriment le même espace de solutions. La différence est structurelle — le mode Array traite la grille comme une fonction (utile si on raisonne sur des cellules arbitraires ou des mises à jour Store), le mode Constants traite la grille comme un tableau de scalaires (plus direct, plus lisible). Ce notebook résout le même Sudoku dans les deux modes et vérifie qu’ils convergent.

2. La grille 4x4 et ses contraintes canoniques

Fixons d’abord une instance avec quelques givens (cellules pré-remplies) pour garantir une solution unique et pouvoir comparer. La grille suivante a trois givens ; le solveur doit compléter le reste.

+---+---+---+---+
| 1 | . | . | . |
+---+---+---+---+
| . | . | . | 3 |
+---+---+---+---+
| . | . | 2 | . |
+---+---+---+---+
| . | 4 | . | . |
+---+---+---+---+

Les contraintes canoniques (identiques dans les deux modes) : 1. Domaine : chaque cellule ∈ {1, 2, 3, 4}. 2. Rangées : les 4 cellules de chaque rangée sont distinctes. 3. Colonnes : les 4 cellules de chaque colonne sont distinctes. 4. Blocs 2x2 : les 4 cellules de chaque bloc sont distinctes. 5. Givens : les cellules pré-remplies sont fixées.

3. Résolution en mode `Constants` (un `Int` par cellule)

Le mode le plus direct : on crée 16 variables Int organisées en matrice 4x4, puis on pose les contraintes Sudoku canoniques. C’est l’encodage idiomatique pyz3 pour un problème sur une grille fixe.

# Mode Constants : 16 Int constants (matrice 4x4).
N = 4
CONST = [[Int(f"c_{r}_{c}") for c in range(N)] for r in range(N)]

s_const = Solver()

# (1) Domaine 1..4 pour chaque cellule.
for r in range(N):
    for c in range(N):
        s_const.add(CONST[r][c] >= 1, CONST[r][c] <= N)

# (2) Rangées : valeurs distinctes.
for r in range(N):
    s_const.add(Distinct(CONST[r]))

# (3) Colonnes : valeurs distinctes.
for c in range(N):
    s_const.add(Distinct([CONST[r][c] for r in range(N)]))

# (4) Blocs 2x2 : valeurs distinctes (N=4 -> blocs de taille 2).
B = 2  # taille de bloc (sqrt(N))
for br in range(0, N, B):
    for bc in range(0, N, B):
        bloc = [CONST[br + i][bc + j] for i in range(B) for j in range(B)]
        s_const.add(Distinct(bloc))

# (5) Givens : (rangée, colonne) -> valeur.
GIVENS = {(0, 0): 1, (1, 3): 3, (2, 2): 2, (3, 1): 4}
for (r, c), v in GIVENS.items():
    s_const.add(CONST[r][c] == v)

print("Mode Constants - statut :", s_const.check())
m_const = s_const.model()
sol_const = [[m_const.eval(CONST[r][c]).as_long() for c in range(N)] for r in range(N)]
print("Solution (Constants) :")
for row in sol_const:
    print("  ", row)

Mode Constants - statut : sat
Solution (Constants) :
   [1, 3, 4, 2]
   [4, 2, 1, 3]
   [3, 1, 2, 4]
   [2, 4, 3, 1]

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

Le mode alternatif : la grille entière est un seul Array(Int, Int) où l’indice r*4 + c désigne la cellule (r, c). On accède aux cellules via Select (voir Z3-Python-17 Array Theory). Les contraintes sont les mêmes, mais exprimées sur des Select(grid, i) plutôt que sur des scalaires.

# Mode Array : un Array(Int, Int) indexe par r*4+c.
grid = Array("grid", IntSort(), IntSort())

s_arr = Solver()

def cell(r, c):
    """Select de la cellule (r,c) dans le tableau symbolique."""
    return Select(grid, r * N + c)

# (1) Domaine 1..4 pour chaque cellule.
for r in range(N):
    for c in range(N):
        s_arr.add(cell(r, c) >= 1, cell(r, c) <= N)

# (2) Rangées distinctes.
for r in range(N):
    s_arr.add(Distinct([cell(r, c) for c in range(N)]))

# (3) Colonnes distinctes.
for c in range(N):
    s_arr.add(Distinct([cell(r, c) for r in range(N)]))

# (4) Blocs 2x2 distincts.
for br in range(0, N, B):
    for bc in range(0, N, B):
        bloc = [cell(br + i, bc + j) for i in range(B) for j in range(B)]
        s_arr.add(Distinct(bloc))

# (5) Givens (memes que le mode Constants).
for (r, c), v in GIVENS.items():
    s_arr.add(cell(r, c) == v)

print("Mode Array - statut :", s_arr.check())
m_arr = s_arr.model()
sol_arr = [[m_arr.eval(cell(r, c)).as_long() for c in range(N)] for r in range(N)]
print("Solution (Array) :")
for row in sol_arr:
    print("  ", row)

Mode Array - statut : sat
Solution (Array) :
   [1, 3, 4, 2]
   [4, 2, 1, 3]
   [3, 1, 2, 4]
   [2, 4, 3, 1]

5. Vérification — les deux solutions sont des carrés latins valides (et coïncident)

Les deux modes doivent produire des grilles qui satisfont toutes les contraintes Sudoku (domaine, rangées, colonnes, blocs, givens). Vérifions le programmatoirement, puis comparons les deux solutions. Avec les mêmes givens et (probablement) une solution unique, elles doivent coïncider exactement.

# Verification : chaque solution est un carre latin Sudoku 4x4 valide.
def est_valide_sudoku(sol):
    """Retourne True si sol est une grille Sudoku 4x4 valide."""
    # Domaine + valeurs entieres 1..4.
    if not all(1 <= sol[r][c] <= N for r in range(N) for c in range(N)):
        return False
    # Rangées.
    if any(len(set(sol[r])) != N for r in range(N)):
        return False
    # Colonnes.
    if any(len({sol[r][c] for r in range(N)}) != N for c in range(N)):
        return False
    # Blocs 2x2.
    for br in range(0, N, B):
        for bc in range(0, N, B):
            bloc = {sol[br + i][bc + j] for i in range(B) for j in range(B)}
            if len(bloc) != N:
                return False
    # Givens respectés.
    if any(sol[r][c] != v for (r, c), v in GIVENS.items()):
        return False
    return True

print("Solution Constants valide :", est_valide_sudoku(sol_const))
print("Solution Array valide      :", est_valide_sudoku(sol_arr))
print("Les deux solutions coïncident :", sol_const == sol_arr)

Solution Constants valide : True
Solution Array valide      : True
Les deux solutions coïncident : True

Interprétation — pourquoi les deux modes convergent

Les deux solutions coïncident (ou sont toutes deux valides si plusieurs solutions existent) : c’est la preuve directe que l’encodage ne change pas le problème. Le mode Constants et le mode Array sont deux syntaxes différentes pour le même ensemble de contraintes — le solveur Z3 les réécrit toutes deux vers le même noyau SMT avant la résolution.

Le choix entre les deux modes est donc une décision de lisibilité et de contexte, pas de correction : - Constants est plus lisible pour une grille fixe (on nomme chaque cellule), et c’est l’encodage idiomatique pyz3. - Array est pertinent dès qu’on veut raisonner sur des cellules arbitraires (indice calculé) ou des mises à jour (Store pour simuler un coup), ou raisonner sur une grille non bornée.

Verdict honnête (Prong-B) : sur un Sudoku 4x4, les deux modes se résolvent instantanément — la différence de performance est invisible. La comparaison devient discriminante sur des grilles plus grandes (9x9) ou quand l’encodage Array permet des raccourcis de modélisation qu’une explosion de Constants (81 variables nommées) rendrait illisibles.

Exercices

Les exercices vous font réutiliser les deux modes sur de nouvelles instances. Chaque exercice suit le squelette : choisir un mode, poser les contraintes canoniques (domaine, rangées, colonnes, blocs, givens), appeler check() puis lire le modèle.

Rappel C.1 : les stubs ne lèvent jamais d’erreur — print("Exercice à compléter"). Le notebook s’exécute de bout en bout même exercices non résolus.

Exercice 1 — Ajouter un hint dans les deux modes

Reprenez la grille 4x4 ci-dessus et ajoutez un cinquième given (par exemple c_0_2 == 4) dans les deux modes (Constants et Array). Vérifiez que les deux solutions coïncident toujours. La solution change-t-elle par rapport à la grille à 4 givens ?

Indice : il suffit d’ajouter une contrainte == supplémentaire dans chaque solveur, puis de relancer check().

# EXERCICE 1 : ajouter un 5e given dans les deux modes.
# TODO etudiant :
# 1. Reprendre s_const et s_arr (ou les re-creer), ajouter CONST[0][2] == 4 et cell(0,2) == 4
# 2. s_const.check() / s_arr.check(), lire les modeles
# 3. Comparer : les deux solutions coïncident-elles ? differentes de la grille a 4 givens ?
print("Exercice 1 a completer : ajouter un 5e given (c_0_2 == 4) dans les deux modes et comparer.")

Exercice 1 a completer : ajouter un 5e given (c_0_2 == 4) dans les deux modes et comparer.

Exercice 2 — Sudoku 9x9 en mode `Constants`

Généralisez le mode Constants à un Sudoku 9x9 (valeurs 1..9, blocs 3x3). Posez les contraintes canoniques pour une grille vide (sans givens) et demandez une solution au solveur. Affichez la grille complète obtenue.

Indice : N = 9, B = 3, même structure de boucles (domaine, rangées Distinct, colonnes, blocs). Une grille vide a de nombreuses solutions — le solveur en produit une.

# EXERCICE 2 : Sudoku 9x9 en mode Constants (grille vide).
# TODO etudiant :
# 1. N = 9, B = 3 ; C9 = [[Int(f"x_{r}_{c}") for c in range(N)] for r in range(N)]
# 2. Domaine 1..9, rangées/colonnes/blocs 3x3 Distinct
# 3. s.check(), afficher la grille 9x9 solution
print("Exercice 2 a completer : Sudoku 9x9 mode Constants, grille vide -> une solution.")

Exercice 2 a completer : Sudoku 9x9 mode Constants, grille vide -> une solution.

Exercice 3 — Comparaison empirique des deux modes

Mesurez le temps de résolution (time.perf_counter() avant/après check()) du Sudoku 4x4 dans chacun des deux modes. Lancez chaque résolution disons 100 fois et comparez les temps moyens. Le mode Array est-il plus lent, plus rapide, ou équivalent au mode Constants ?

Question subsidiaire : pourquoi le mode Array pourrait-il être (légèrement) plus lent sur une grille fixe, alors qu’il est plus expressif sur une grille dynamique ?

# EXERCICE 3 : comparaison empirique des temps de résolution (Constants vs Array).
# TODO etudiant :
# 1. Pour chaque mode : construire le solver, mesurer t0 = time.perf_counter(), s.check(), t1
# 2. Repeter 100 fois, moyenner
# 3. Afficher : temps moyen Constants vs Array, verdict
print("Exercice 3 a completer : mesurer et comparer les temps moyens Constants vs Array (100 runs).")

Exercice 3 a completer : mesurer et comparer les temps moyens Constants vs Array (100 runs).

Conclusion

Ce notebook démontre le principe fondamental de la modélisation SMT : le problème (les contraintes) est séparé de l’encodage (comment on les exprime). Deux encodages radicalement différents — 16 Int constants vs un Array(Int, Int) — du même Sudoku 4x4 convergent vers la même solution valide.

Aspect	Mode `Constants`	Mode `Array`
Structure	16 scalaires nommés	1 fonction Index → Valeur
Accès cellule	`CONST[r][c]`	`Select(grid, r*4+c)`
Lisibilité grille fixe	Excellente	Moyenne
Cellule arbitraire / mise à jour	Malaisé (nom fixe)	Naturel (`Store`)
Sémantique (solutions)	Identique	Identique

Leçon : choisir l’encodage selon le contexte de raisonnement (grille fixe vs dynamique), pas selon une prétendue « meilleure » représentation. Le solveur réécrit tout vers le même noyau SMT — la correction est garantie par les contraintes, pas par la syntaxe.

Retour au sommet