Sudoku-12-Z3-Python : Z3 SMT Solver (Python)

Navigation : << OR-Tools Python | Index | Infer Python >>

Objectifs d’apprentissage

A la fin de ce notebook, vous saurez : 1. Modeliser le Sudoku avec un solveur SMT (Z3) 2. Comprendre la différence entre SAT et SMT 3. Utiliser des BitVectors pour optimiser les representations 4. Comparer Z3 Int avec Z3 BitVector

Duree estimee : ~10 min | Prerequis : Sudoku-00 Environment

Ce notebook implemente un solveur de Sudoku utilisant Z3 (prouveur SMT issu de Microsoft Research, desormais open-source sous licence MIT), un solveur SMT (Satisfiable Modulo Theories).

Cette approche est equivalente au notebook C# Sudoku-12-Z3-CSharp.ipynb.

Installation

pip install z3-solver

# Imports
import time
from typing import List, Optional, Tuple
from pathlib import Path

# Verifier l'installation
try:
    from z3 import *
    print(f"Z3 importe avec succes")
except ImportError:
    print("Z3 non installe. Executez: pip install z3-solver")

Z3 importe avec succes

1. Solveur Z3 SMT

Z3 est un solveur SMT (Satisfiability Modulo Theories) developpe a l’origine par Microsoft Research (Leonardo de Moura et Nikolaj Bjorner), desormais publie en open-source sous licence MIT dans le depot Z3Prover/z3. Il combine la puissance des solveurs SAT avec des theories mathematiques (arithmetique, tableaux, bitvectors, etc.).

Source et licence. Z3 est un prouveur de theoremes issu de Microsoft Research, desormais libre (licence MIT) sur github.com/Z3Prover/z3. Reference canonique : Leonardo de Moura et Nikolaj Bjorner, Z3: An Efficient SMT Solver, in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008. Ce notebook distille cette source au travers du prisme pedagogique du Sudoku : il ne reproduit ni l’article ni la documentation officielle, mais demontre l’API Python z3-solver (Int, BitVec, Solver, Optimize) sur un exemple concret.

Différence entre SAT et SMT

SAT	SMT
Variables booléennes uniquement	Variables typées (Int, Real, BitVec, Array…)
Clauses propositionnelles	Formules de premier ordre
`(x OR y) AND (NOT x OR z)`	`x + y > 10 AND x < 5`

2. Configuration du chemin vers les puzzles

# Configuration du chemin vers les puzzles
import os

# Definir le chemin absolu vers le dossier Puzzles
NOTEBOOK_DIR = Path.cwd()
PUZZLES_DIR = NOTEBOOK_DIR / "Puzzles"

# Verifier que le dossier existe
if PUZZLES_DIR.exists():
    print(f"Dossier Puzzles: {PUZZLES_DIR}")
    puzzle_files = list(PUZZLES_DIR.glob('*.txt'))
    print(f"Fichiers disponibles: {[f.name for f in puzzle_files]}")
else:
    print(f"ATTENTION: Dossier Puzzles non trouve a {PUZZLES_DIR}")
    PUZZLES_DIR = Path(os.getcwd()) / "Puzzles"

Dossier Puzzles: <repo>MyIA.AI.Notebooks\Sudoku\Puzzles
Fichiers disponibles: ['Sudoku_Easy51.txt', 'Sudoku_hardest.txt', 'Sudoku_top95.txt']

3. Solveurs Z3 : Int et BitVector

Nous presentons deux approches pour encoder le Sudoku avec Z3 :

Z3 Int : variables entieres symboliques (Int), encodage classique.
Z3 BitVector : variables BitVec 4 bits, optimisation pour plages bornees.

Nous definissons d’abord une representation de la grille, puis comparons les deux encodages sur les mêmes puzzles.

Representation de la grille Sudoku avec fonctions de chargement.

class SudokuGrid:
    """Représentation d'une grille de Sudoku 9x9."""
    
    def __init__(self, grid: Optional[List[List[int]]] = None):
        if grid is None:
            self.cells = [[0] * 9 for _ in range(9)]
        else:
            self.cells = [row[:] for row in grid]
    
    @classmethod
    def from_string(cls, s: str) -> 'SudokuGrid':
        s = s.replace('.', '0').replace(' ', '').replace('\n', '')
        if len(s) != 81:
            raise ValueError(f"La chaîne doit avoir 81 caractères")
        grid = cls()
        for i in range(81):
            grid.cells[i // 9][i % 9] = int(s[i])
        return grid
    
    def clone(self) -> 'SudokuGrid':
        return SudokuGrid(self.cells)
    
    def __str__(self) -> str:
        lines = []
        for r in range(9):
            if r > 0 and r % 3 == 0:
                lines.append('-' * 21)
            row_str = ''
            for c in range(9):
                if c > 0 and c % 3 == 0:
                    row_str += '| '
                val = self.cells[r][c]
                row_str += (str(val) if val != 0 else '.') + ' '
            lines.append(row_str)
        return '\n'.join(lines)

def load_puzzles(filepath: str, max_puzzles: int = None) -> List[str]:
    puzzles = []
    with open(filepath, 'r') as f:
        for line in f:
            line = line.strip()
            if len(line) >= 81:
                puzzles.append(line[:81])
                if max_puzzles and len(puzzles) >= max_puzzles:
                    break
    return puzzles

# Charger puzzles
easy_puzzles = load_puzzles(str(PUZZLES_DIR / 'Sudoku_Easy51.txt'), max_puzzles=10)
hard_puzzles = load_puzzles(str(PUZZLES_DIR / 'Sudoku_hardest.txt'))
print(f"Puzzles chargés: {len(easy_puzzles)} faciles, {len(hard_puzzles)} difficiles")

Puzzles chargés: 10 faciles, 11 difficiles

Lecture du corpus : trois fichiers, 10 faciles + 11 difficiles

La sortie énumère le contenu du dossier commun de la série — Easy51, hardest, top95 — puis la classe de chargement en tire 10 faciles et 11 difficiles. Ce sont les mêmes corpus que le benchmark du notebook Sudoku-07-Norvig-Python (20 faciles à 3,30 ms, 11 difficiles à 4,45 ms par propagation) : les encodages diffèrent, les terrains de jeu non. Le puzzle difficile affiché en tête de test (8 5 . | . . 2 | 4 . . …) est l’exemplaire sur lequel le solveur Int de la section suivante sera mesuré à ~340,86 ms sur cette machine (mesure live sortie [12] ; ordre de grandeur stable cross-machine, valeur exacte dependante du hardware, règle #9434).

Definition du solveur Z3 pour Sudoku.

class Z3Solver:
    """Solveur Sudoku utilisant Z3 SMT."""
    
    def solve(self, grid: SudokuGrid) -> bool:
        """Résout le Sudoku avec Z3."""
        # Créer les variables: X[i][j] est un entier 1-9
        X = [[Int(f'x_{i}_{j}') for j in range(9)] for i in range(9)]
        
        solver = Solver()
        
        # Contraintes de domaine: 1 <= X[i][j] <= 9
        for i in range(9):
            for j in range(9):
                solver.add(X[i][j] >= 1, X[i][j] <= 9)
        
        # Valeurs initiales
        for i in range(9):
            for j in range(9):
                if grid.cells[i][j] != 0:
                    solver.add(X[i][j] == grid.cells[i][j])
        
        # Contraintes: toutes différentes par ligne
        for i in range(9):
            solver.add(Distinct([X[i][j] for j in range(9)]))
        
        # Contraintes: toutes différentes par colonne
        for j in range(9):
            solver.add(Distinct([X[i][j] for i in range(9)]))
        
        # Contraintes: toutes différentes par bloc 3x3
        for box_row in range(3):
            for box_col in range(3):
                box_cells = []
                for i in range(3):
                    for j in range(3):
                        box_cells.append(X[box_row * 3 + i][box_col * 3 + j])
                solver.add(Distinct(box_cells))
        
        # Résoudre
        if solver.check() == sat:
            model = solver.model()
            for i in range(9):
                for j in range(9):
                    grid.cells[i][j] = model.evaluate(X[i][j]).as_long()
            return True
        
        return False

# Test
z3_solver = Z3Solver()
test_grid = SudokuGrid.from_string(hard_puzzles[0])
print("Puzzle difficile:")
print(test_grid)

start = time.time()
solved = z3_solver.solve(test_grid)
elapsed = (time.time() - start) * 1000

print(f"\nRésolu: {solved} en {elapsed:.2f} ms")
print("\nSolution:")
print(test_grid)

Puzzle difficile:
8 5 . | . . 2 | 4 . . 
7 2 . | . . . | . . 9 
. . 4 | . . . | . . . 
---------------------
. . . | 1 . 7 | . . 2 
3 . 5 | . . . | 9 . . 
. 4 . | . . . | . . . 
---------------------
. . . | . 8 . | . 7 . 
. 1 7 | . . . | . . . 
. . . | . 3 6 | . 4 . 

Résolu: True en 340.86 ms

Solution:
8 5 9 | 6 1 2 | 4 3 7 
7 2 3 | 8 5 4 | 1 6 9 
1 6 4 | 3 7 9 | 5 2 8 
---------------------
9 8 6 | 1 4 7 | 3 5 2 
3 7 5 | 2 6 8 | 9 1 4 
2 4 1 | 5 9 3 | 7 8 6 
---------------------
4 3 2 | 9 8 1 | 6 7 5 
6 1 7 | 4 2 5 | 8 9 3 
5 9 8 | 7 3 6 | 2 4 1

Interpretation : Résultat Z3 Int

Le solveur Z3 avec des entiers a resolu le puzzle difficile quasi-instantanement (temps mesure dynamiquement par la cellule de code ci-dessus).

Aspect	Valeur	Signification
Statut	sat	Solution trouvee
Type de variables	Int	Entiers symboliques

Points cles : 1. API simple : La contrainte Distinct est très expressive 2. Théorie des entiers : Z3 utilise QF_LIA (Linear Integer Arithmetic) 3. Flexibilite : Z3 peut facilement etendre le modèle avec d’autres contraintes

Note technique : La contrainte Distinct de Z3 est plus puissante que l’inegalite binaire car elle permet au solveur d’utiliser des algorithmes specialised pour la propagation.

Regle #9434 : le temps de resolution (machine-dependant) est mesure dynamiquement par la cellule de code ci-dessus ; il n’est pas fige ici.

Exercice : Contrainte de somme sur un bloc (Killer Sudoku)

Le solveur Z3 avec Int permet d’ajouter facilement des contraintes arithmetiques. Le Killer Sudoku est une variante ou des groupes de cellules doivent satisfaire une somme cible. Implementez un solveur qui ajoute une contrainte Sum(valeurs du bloc) == target_sum sur un bloc 3x3 spécifique. La somme naturelle d’un bloc est 1+2+…+9 = 45.

def solve_with_sum_constraint(grid: SudokuGrid, block_row: int, block_col: int, target_sum: int) -> bool:
    """
    Resout un Sudoku avec une contrainte supplementaire de somme sur un bloc 3x3.

    Cette variante s'inspire du "Killer Sudoku" ou des groupes de cellules
    doivent satisfaire une contrainte arithmetique en plus des regles classiques.

    Args:
        grid: Grille a resoudre (0 = case vide)
        block_row: Ligne du bloc (0, 1 ou 2)
        block_col: Colonne du bloc (0, 1 ou 2)
        target_sum: Somme cible pour les 9 valeurs du bloc

    Returns:
        True si solution trouvee, False sinon
    """
    # TODO etudiant : implementer la contrainte de somme sur un bloc
    # Etape 1 : creer le Solver Z3 et les 81 variables Int (domaine [1,9])
    # Etape 2 : ajouter les 27 contraintes Distinct (lignes, colonnes, blocs)
    # Etape 3 : fixer les valeurs initiales de la grille
    # Etape 4 : calculer les coordonnees du bloc (block_row*3 + i, block_col*3 + j)
    # Etape 5 : ajouter la contrainte Sum(cells du bloc) == target_sum
    # Etape 6 : resoudre et mettre a jour la grille si solution trouvee
    return False  # TODO etudiant : remplacer par la resolution reelle

print("Exercice a completer : contrainte de somme sur bloc")

Exercice a completer : contrainte de somme sur bloc

Passage au solveur BitVector (objectif 4 : comparer les deux encodages).

class Z3BitVectorSolver:
    """Solveur Z3 utilisant des BitVectors 4 bits."""
    
    def solve(self, grid: SudokuGrid) -> bool:
        """Résout avec BitVectors."""
        # BitVectors 4 bits (valeurs 1-9 tiennent dans 4 bits)
        X = [[BitVec(f'x_{i}_{j}', 4) for j in range(9)] for i in range(9)]
        
        solver = Solver()
        
        # Contraintes de domaine
        for i in range(9):
            for j in range(9):
                solver.add(UGE(X[i][j], 1))  # >= 1 (unsigned)
                solver.add(ULE(X[i][j], 9))  # <= 9 (unsigned)
        
        # Valeurs initiales
        for i in range(9):
            for j in range(9):
                if grid.cells[i][j] != 0:
                    solver.add(X[i][j] == grid.cells[i][j])
        
        # Contraintes Distinct (par paires pour BitVec)
        def add_all_different(cells):
            for i in range(len(cells)):
                for j in range(i + 1, len(cells)):
                    solver.add(cells[i] != cells[j])
        
        # Lignes
        for i in range(9):
            add_all_different([X[i][j] for j in range(9)])
        
        # Colonnes
        for j in range(9):
            add_all_different([X[i][j] for i in range(9)])
        
        # Blocs
        for box_row in range(3):
            for box_col in range(3):
                box_cells = [X[box_row * 3 + i][box_col * 3 + j] 
                             for i in range(3) for j in range(3)]
                add_all_different(box_cells)
        
        if solver.check() == sat:
            model = solver.model()
            for i in range(9):
                for j in range(9):
                    grid.cells[i][j] = model.evaluate(X[i][j]).as_long()
            return True
        
        return False

# Comparaison Z3 Int vs BitVec
print("=== Comparaison Z3 Int vs BitVector ===")

z3_int = Z3Solver()
z3_bv = Z3BitVectorSolver()

for i, puzzle_str in enumerate(hard_puzzles[:5]):
    print(f"\nPuzzle {i+1}:")
    
    grid1 = SudokuGrid.from_string(puzzle_str)
    start = time.time()
    z3_int.solve(grid1)
    t1 = (time.time() - start) * 1000
    
    grid2 = SudokuGrid.from_string(puzzle_str)
    start = time.time()
    z3_bv.solve(grid2)
    t2 = (time.time() - start) * 1000
    
    print(f"  Z3 Int:      {t1:>8.2f} ms")
    print(f"  Z3 BitVec:   {t2:>8.2f} ms")

=== Comparaison Z3 Int vs BitVector ===

Puzzle 1:
  Z3 Int:        271.18 ms
  Z3 BitVec:      68.65 ms

Puzzle 2:
  Z3 Int:        462.26 ms
  Z3 BitVec:      71.84 ms

Puzzle 3:
  Z3 Int:        222.89 ms
  Z3 BitVec:      61.95 ms

Puzzle 4:
  Z3 Int:        389.18 ms
  Z3 BitVec:     117.54 ms

Puzzle 5:
  Z3 Int:        237.59 ms
  Z3 BitVec:     105.18 ms

Interpretation : Z3 Int vs BitVector

La comparaison montre que l’utilisation de BitVectors 4 bits est significativement plus rapide que les entiers — le gain observe est de ~2x a ~6x selon le puzzle (ordre de grandeur stable cross-machine, mesure dynamiquement par la cellule de benchmark ci-dessus).

Puzzle	Amelioration (BitVec vs Int)
Puzzle 1	~4x plus rapide
Puzzle 2	~6x plus rapide
Puzzle 3	~4x plus rapide
Puzzle 4	~3x plus rapide
Puzzle 5	~2x plus rapide

Points cles : 1. BitVectors sont plus proches du hardware : Z3 peut utiliser des opérations bit-level 2. Domaine restreint : 4 bits = 16 valeurs, exactement ce qu’il faut pour 1-9 3. Propagation plus efficace : Les contraintes bit-level sont plus simples a propager

Note technique : Les BitVectors sont representes en precision fixe (4 bits ici), ce qui permet a Z3 d’utiliser des algorithmes de propagation plus efficaces. Les entiers symboliques en Z3 ont une precision arbitraire, ce qui ajoute de la complexite.

Regle #9434 : les temps absolus (machine-dependants) sont mesures dynamiquement par la cellule de benchmark ci-dessus ; seuls les ordres de grandeur du speedup (structurels, stables cross-machine) sont conserves ici.

4. Resume et conclusions

Ce notebook a presente deux approches Z3 pour resoudre le Sudoku : avec des entiers symboliques et avec des BitVectors.

Comparaison des approches Z3

Approche	Type	Avantages	Inconvenients
Z3 Int	Entiers symboliques	API simple, contrainte `Distinct` expressive	Plus lent
Z3 BitVec	BitVectors 4 bits	Plus rapide, proche du hardware	Syntaxe plus complexe

Recommandations

Simplicite : Z3 Int avec la contrainte Distinct
Performance : Z3 BitVec pour les domaines restreints
Flexibilite : Z3 supporte de nombreuses théories (arithmetique, tableaux, etc.)

Au-dela du Sudoku

Z3 peut resoudre une grande variete de problemes : - Verification de programmes - Analyse de securite - Synthese de code - Theoremes de logique

Le Sudoku est un excellent problème pedagogique pour comprendre la différence entre SAT (propositionnel) et SMT (théories).

5. Exercices et exemples guides

Cette section contient :

Exercice 1 : compter le nombre de solutions d’une grille donnee (a implementer)
Exemple guide : solveur Z3 avec contrainte diagonale (solution fournie pour reference)
Exercice 2 : coloration de graphe avec Z3 (a implementer)
Exemple guide : Optimisation SMT avec Optimize / maximize (carre latin a reward maximal, solution complete)
Exercice 3 : minimiser un cout diagonal avec Optimize (a implementer)
Conclusion : bilan comparatif Int vs BitVec et ouverture SMT

Chaque bloc est clairement marque comme “exercice” (a completer) ou “exemple” (solution complete).

Exercice 1 : Compter le nombre de solutions

Implementez un solveur Z3 qui compte le nombre total de solutions d’une grille de Sudoku.

Indices : - Utiliser Solver() et ajouter les contraintes classiques - Après chaque s.check() == sat, ajouter une contrainte excluant le modèle trouve (s.add(Not(And([cells[r][c] == m.evaluate(cells[r][c]) for r in range(9) for c in range(9)])))) - Compter les itérations jusqu’a unsat

# TODO: Implementer Z3SolutionCounter
#
# Probleme : compter le nombre de solutions d'une grille Sudoku
# jusqu'a un maximum donne (par ex. 10).
#
# Indices :
# - Reutilisez la structure de Z3Solver (Solver, cells Int, Distinct
#   pour lignes/colonnes/blocs, contraintes de domaine et valeurs fixees).
# - Apres chaque s.check() == sat, recuperez m = s.model() et bloquez
#   cette solution avec :
#       s.add(Or([cells[r][c] != m.evaluate(cells[r][c])
#                 for r in range(9) for c in range(9)]))
# - Iterez jusqu'a atteindre max_count ou unsat.


class Z3SolutionCounter:
    """Solver Z3 qui compte les solutions jusqu'a un maximum."""

    def count_solutions(self, grid: SudokuGrid, max_count: int = 10) -> int:
        """
        Compte le nombre de solutions jusqu'a max_count.

        Args:
            grid: Grille de Sudoku a resoudre
            max_count: Nombre maximum de solutions a chercher

        Returns:
            Nombre de solutions trouvees (<= max_count)
        """
        # TODO: Implementer
        # 1. Creer Solver() et les variables Z3 (Int)
        # 2. Ajouter contraintes Sudoku (domaine, valeurs fixees, lignes/colonnes/blocs)
        # 3. Boucle : check(), bloquer solution trouvee, incrementer compteur
        pass


# Test
counter = Z3SolutionCounter()
test_grid = SudokuGrid.from_string(easy_puzzles[0])
result = counter.count_solutions(test_grid)
if result is not None:
    print(f"Nombre de solutions (max 10): {result}")
else:
    print("Implementation a completer pour voir le resultat")

Implementation a completer pour voir le resultat

Exemple guide : Solveur Z3 avec contrainte diagonale

L’implementation ci-dessous etend le solver Z3 classique en ajoutant les contraintes Distinct sur les deux diagonales principales.

# Implementation : Z3DiagonalSolver
# Contraintes supplementaires pour les diagonales:
# - Diagonale principale: cells[i][i] pour i in 0..8
# - Diagonale secondaire: cells[i][8-i] pour i in 0..8

class Z3DiagonalSolver:
    """
    Solver Z3 pour Sudoku avec contraintes diagonales supplementaires.
    """
    
    def solve(self, grid: SudokuGrid) -> bool:
        """Resout le Sudoku diagonal avec Z3."""
        # Contraintes diagonales
        s = Solver()

        # Variables
        cells = [[Int(f"c_{r}_{c}") for c in range(9)] for r in range(9)]

        # Domaine [1..9]
        for r in range(9):
            for c in range(9):
                s.add(cells[r][c] >= 1, cells[r][c] <= 9)

        # Valeurs fixées
        for r in range(9):
            for c in range(9):
                if grid.cells[r][c] != 0:
                    s.add(cells[r][c] == grid.cells[r][c])

        # Contraintes classiques : lignes, colonnes, blocs
        for i in range(9):
            s.add(Distinct(cells[i]))
            s.add(Distinct([cells[r][i] for r in range(9)]))

        for br in range(3):
            for bc in range(3):
                s.add(Distinct([cells[br*3 + r][bc*3 + c]
                                for r in range(3) for c in range(3)]))

        # Contraintes diagonales
        s.add(Distinct([cells[i][i] for i in range(9)]))      # diagonale principale
        s.add(Distinct([cells[i][8 - i] for i in range(9)]))  # diagonale secondaire

        # Résolution
        if s.check() == sat:
            m = s.model()
            for r in range(9):
                for c in range(9):
                    grid.cells[r][c] = m.evaluate(cells[r][c]).as_long()
            return True
        return False


# Test avec une grille diagonale
diagonal_solver = Z3DiagonalSolver()

test = ("100000000"
"000003000"
"080005020"
"231000000"
"060000000"
"097000231"
"000978000"
"000000000"
"078000000"
)

diag_grid = SudokuGrid.from_string(test)
print("Grille avant résolution :")
print(diag_grid)
print()

if diagonal_solver.solve(diag_grid):
    print("Solution trouvée :")
    print(diag_grid)
    # Vérification des diagonales
    diag1 = [diag_grid.cells[i][i] for i in range(9)]
    diag2 = [diag_grid.cells[i][8 - i] for i in range(9)]
    print(f"\nDiagonale principale : {diag1} — tous distincts : {len(set(diag1)) == 9}")
    print(f"Diagonale secondaire : {diag2} — tous distincts : {len(set(diag2)) == 9}")
else:
    print("Pas de solution")

Grille avant résolution :
1 . . | . . . | . . . 
. . . | . . 3 | . . . 
. 8 . | . . 5 | . 2 . 
---------------------
2 3 1 | . . . | . . . 
. 6 . | . . . | . . . 
. 9 7 | . . . | 2 3 1 
---------------------
. . . | 9 7 8 | . . . 
. . . | . . . | . . . 
. 7 8 | . . . | . . . 

Solution trouvée :
1 2 5 | 4 8 7 | 6 9 3 
6 4 9 | 2 1 3 | 8 7 5 
7 8 3 | 6 9 5 | 1 2 4 
---------------------
2 3 1 | 7 5 9 | 4 6 8 
8 6 4 | 3 2 1 | 9 5 7 
5 9 7 | 8 4 6 | 2 3 1 
---------------------
3 1 6 | 9 7 8 | 5 4 2 
9 5 2 | 1 3 4 | 7 8 6 
4 7 8 | 5 6 2 | 3 1 9 

Diagonale principale : [1, 4, 3, 7, 2, 6, 5, 8, 9] — tous distincts : True
Diagonale secondaire : [3, 7, 1, 9, 2, 8, 6, 5, 4] — tous distincts : True

Lecture du solveur diagonal : deux contraintes de plus, rien d’autre

Comparez les deux grilles affichées : la grille d’entrée est clairsemée (une vingtaine d’indices), et la solution est trouvée avec les deux diagonales vérifiées toutes-distinctes — principale [1, 4, 3, 7, 2, 6, 5, 8, 9], secondaire [3, 7, 1, 9, 2, 8, 6, 5, 4], toutes deux True. C’est la variante Sudoku-X, et la leçon est dans le code : passer du Sudoku standard au Sudoku-X a coûté exactement deux lignes — deux Distinct supplémentaires sur les diagonales cells[i][i] et cells[i][8-i]. Aucune heuristique à ré-accorder, aucun solveur à ré-écrire : c’est l’additivité déclarative du SMT, la propriété qui le distingue d’un solveur dédié (le backtracking de Sudoku-13 exige de toucher la fonction de validité pour la même variante).

Exercice 2 : Coloration de graphe avec Z3

Z3 n’est pas limite au Sudoku ! Il peut resoudre de nombreux problemes de satisfaction de contraintes.

Objectif : Implementer un solveur de coloration de graphe (graph coloring) avec Z3.

Le problème consiste a colorier une carte de regions avec un nombre minimum de couleurs, de sorte que deux regions voisines (partageant une frontiere) n’aient jamais la même couleur.

Theoreme des 4 couleurs : toute carte plane peut etre coloriee avec au plus 4 couleurs.

Étapes : 1. Modeliser chaque region par une variable entiere Int representant sa couleur (0 a 3) 2. Ajouter les contraintes de domaine : 0 <= couleur <= 3 3. Pour chaque paire de regions voisines, ajouter la contrainte couleur_i != couleur_j 4. Resoudre avec solver.check() == sat et extraire la coloration

Code a completer dans la cellule suivante

# TODO: Implementer un solveur de coloration de graphe avec Z3
#
# Probleme : colorier les regions de la carte de France metropolitaine
# avec 4 couleurs, de sorte que deux regions voisines n'aient jamais
# la meme couleur.
#
# Indices :
# - Les regions sont representees par des noeuds, les frontieres par des aretes.
# - Utilisez Int(color_i) pour la couleur de chaque region, domaine [0, 3].
# - Pour chaque arete (i, j), ajoutez color_i != color_j.

def solve_graph_coloring():
    """
    Resout le probleme de coloration de graphe avec Z3.
    
    Le graphe represente une partie simplifiee de la carte de France
    avec 10 regions et leurs voisinages.
    
    Returns:
        dict mapping region name -> color (0-3) si solution trouvee, None sinon
    """
    # Graphe : {region: [voisins]}
    regions = {
        "Ile-de-France": ["Picardie", "Normandie", "Centre", "Bourgogne"],
        "Picardie": ["Ile-de-France", "Normandie", "Champagne"],
        "Normandie": ["Ile-de-France", "Picardie", "Bretagne", "Pays-de-la-Loire", "Centre"],
        "Bretagne": ["Normandie", "Pays-de-la-Loire"],
        "Pays-de-la-Loire": ["Bretagne", "Normandie", "Centre", "Aquitaine"],
        "Centre": ["Ile-de-France", "Normandie", "Pays-de-la-Loire", "Aquitaine", "Bourgogne", "Auvergne"],
        "Bourgogne": ["Ile-de-France", "Centre", "Champagne", "Auvergne"],
        "Champagne": ["Picardie", "Bourgogne", "Auvergne"],
        "Auvergne": ["Centre", "Bourgogne", "Champagne", "Aquitaine"],
        "Aquitaine": ["Pays-de-la-Loire", "Centre", "Auvergne"],
    }
    num_colors = 4
    color_names = ["Bleu", "Blanc", "Rouge", "Vert"]
    
    # TODO: Modeliser le probleme avec Z3
    # 1. Creer une variable Int pour chaque region
    # 2. Ajouter les contraintes de domaine [0, num_colors-1]
    # 3. Pour chaque paire de regions voisines, ajouter color_i != color_j
    # 4. Resoudre et retourner le resultat
    
    pass


# Test
result = solve_graph_coloring()
if result:
    print("Coloration trouvee :")
    for region, color in sorted(result.items()):
        print(f"  {region}: {color}")
else:
    print("Pas de solution trouvee")

Pas de solution trouvee

Lecture honnête : « Pas de solution trouvee » = le stub rendu proprement

La ligne unique de la sortie est la sortie conventionnelle d’un exercice incomplet (règle C.1) : la fonction rend None proprement au lieu de lever une erreur, et l’énoncé imprime le diagnostic. Le problème attendu — colorier la carte de France à 10 régions avec 4 couleurs via Int(color_i) et color_i != color_j par arête — est exactement la modélisation du Sudoku transposée : des variables à domaine fini, des contraintes de différence binaire. Le théorème des quatre couleurs garantit qu’une solution existe pour toute carte planaire ; l’exercice, lui, attend sa modélisation.

Exemple guide : Optimisation SMT avec Z3 (`Optimize` / `maximize`)

Jusqu’ici, Z3 a resolu des problemes de satisfaction : trouver UNE solution realisable (une grille de Sudoku valide) via Solver() + check() + model().

La capacite distinctive de Z3 est l’optimisation SMT : le contexte Optimize() resout des problemes ou l’on maximise (ou minimise) un objectif sous contraintes – c’est le moteur de la programmation MaxSMT (maximisation sat-modulo-theories, utilise en verification, scheduling, allocation de ressources, debug de modeles).

Demonstration : un « carre latin a bonus » – chaque cellule (i, j) offre un reward dependant de la valeur placee. Parmi tous les carres latins 5x5 valides, Optimize() + maximize() trouve celui qui maximise le reward total. Le statut sat certifie que l’optimum est atteint (preuve non-vacuous).

Miroir de la demo CP-SAT du notebook Sudoku-10-ORTools-Python (meme probleme, meme reward 178), mais avec l’API SMT z3.Optimize() au lieu de cp_model.CpModel.Maximize().

"""Z3 SMT optimization demo: Optimize() + maximize() on a weighted latin square.

Demonstrates Z3's signature optimization capability (MaxSMT / Optimize context)
which is distinct from satisfaction-only Solver(). Mirrors the CP-SAT
optimization demo in Sudoku-10-ORTools-Python (c.711) but exercises the SMT
solver's distinctive Optimize() API.
"""
import random
import z3


def solve_max_reward_latin_square_z3(n: int = 5, reward=None, seed: int = 42):
    """Find the latin square of order n that MAXIMIZES total reward.

    reward[i][j][v] = bonus for placing value v (1..n) at cell (i, j).
    Uses z3.Optimize() -- the SMT optimization context -- with opt.maximize().
    Returns OPTIMAL solution + objective value (proves no better square exists).
    """
    rng = random.Random(seed)
    if reward is None:
        reward = [[[rng.randint(0, 10) for _ in range(n + 1)] for _ in range(n)] for _ in range(n)]

    opt = z3.Optimize()
    x = {}
    for i in range(n):
        for j in range(n):
            for v in range(1, n + 1):
                x[i, j, v] = z3.Bool(f"x_{i}_{j}_{v}")
            # exactly one value per cell
            opt.add(z3.PbEq([(x[i, j, v], 1) for v in range(1, n + 1)], 1))
        # each value once per row
        for v in range(1, n + 1):
            opt.add(z3.PbEq([(x[i, j, v], 1) for j in range(n)], 1))
    # each value once per column
    for j in range(n):
        for v in range(1, n + 1):
            opt.add(z3.PbEq([(x[i, j, v], 1) for i in range(n)], 1))

    # objective: maximize total reward
    objective = z3.Sum([z3.If(x[i, j, v], reward[i][j][v], 0)
                        for i in range(n) for j in range(n) for v in range(1, n + 1)])
    opt.maximize(objective)

    status = opt.check()
    if status != z3.sat:
        return None, None, str(status)
    model = opt.model()
    grid = [[0] * n for _ in range(n)]
    for i in range(n):
        for j in range(n):
            for v in range(1, n + 1):
                if z3.is_true(model[x[i, j, v]]):
                    grid[i][j] = v
    # recompute objective from grid for a clean numeric value
    # (opt.upper() needs the handle from maximize(); we read it straight off the grid)
    computed = sum(reward[i][j][grid[i][j]] for i in range(n) for j in range(n))
    return grid, computed, "sat"
grid, obj, status = solve_max_reward_latin_square_z3(n=5, seed=42)
print(f"Statut Z3 Optimize : {status}")
print(f"Reward maximal     : {obj}")
print("Carre latin optimal (max reward) :")
for row in grid:
    print(" ".join(f"{v:2d}" for v in row))
n = len(grid)
ok = all(sorted(row) == list(range(1, n + 1)) for row in grid) and \
     all(sorted(grid[i][j] for i in range(n)) == list(range(1, n + 1)) for j in range(n))
print(f"Carre latin valide : {ok}")

Statut Z3 Optimize : sat
Reward maximal     : 178
Carre latin optimal (max reward) :
 3  2  1  5  4
 2  1  5  4  3
 1  4  2  3  5
 5  3  4  1  2
 4  5  3  2  1
Carre latin valide : True

Lecture du Optimize : sat, reward 178, et la preuve d’optimalité

Quatre lignes, quatre enseignements. Statut : sat — le contexte Optimize de Z3 est d’abord un solveur de satisfaction. Reward maximal : 178 — ce n’est pas un reward trouvé, c’est un reward prouvé maximal : Optimize boucle en résolvant puis en ajoutant la contrainte « objectif > meilleur courant » jusqu’à l’insatisfiabilité — la différence entre « une bonne solution » et « la meilleure » est exactement la différence entre Solver et Optimize. Le carré latin 5x5 affiché — chaque ligne et chaque colonne est une permutation de 1-5, vérifié par la ligne « Carre latin valide : True » (citation de la sortie). La docstring de la cellule le dit : ce démo est le miroir SMT de l’exemple CP-SAT du notebook Sudoku-10-ORTools — deux moteurs, une même capacité signature, la maximisation sous contraintes.

Exercice : Minimiser un cout diagonal avec Z3 `Optimize`

Adaptez la modelisation ci-dessus pour MINIMISER une fonction de cout au lieu de maximiser le reward.

Indices : 1. Gardez les memes contraintes (carre latin : PbEq one-value-per-cell, latin rows/cols). 2. Remplacez opt.maximize(reward_total) par : python diagonal_sum = z3.Sum([z3.If(x[i, i, v], v, 0) for i in range(n) for v in range(1, n + 1)]) opt.minimize(diagonal_sum) 3. Objectif : le carre latin 5x5 qui minimise la somme des valeurs sur la diagonale principale (privilegier les petits nombres sur la diagonale). 4. Verifiez que le statut reste sat et que le cout diagonal obtenu est inferieur au reward maximal (178) ci-dessus.

"""Minimize stub (exercise) for Z3 Optimize -- graceful degradation pattern.

Matches the notebook's existing stub convention ([19]/[23]): function returns
None until implemented, caller prints a 'complete this' message. C.1 compliant
(no error), produces a stdout output (C.2).
"""


def solve_min_diagonal_latin_square_z3(n: int = 5, seed: int = 42):
    """TODO: miroir MINIMISE de solve_max_reward_latin_square_z3.

    Objectif : minimiser la somme des valeurs sur la diagonale principale
    (grid[i][i] pour i dans 0..n-1) d'un carre latin 5x5.
    """
    # TODO: copiez solve_max_reward_latin_square_z3 ci-dessus et adaptez :
    #   1. Gardez les memes contraintes (Optimize, PbEq one-value-per-cell,
    #      latin rows/cols).
    #   2. Remplacez opt.maximize(reward_total) par :
    #        diagonal_sum = z3.Sum([z3.If(x[i, i, v], v, 0)
    #                               for i in range(n) for v in range(1, n + 1)])
    #        opt.minimize(diagonal_sum)
    #   3. Retournez (grid, computed_diagonal, "sat").
    return None


result = solve_min_diagonal_latin_square_z3(n=5)
if result is not None:
    grid, cost, status = result
    print(f"Statut : {status} | Cout diagonal minimal : {cost}")
    for row in grid:
        print(" ".join(f"{v:2d}" for v in row))
else:
    print("Implementation a completer pour voir le resultat")

Implementation a completer pour voir le resultat

Conclusion

Ce notebook a présenté deux approches Z3 pour modéliser et résoudre le Sudoku : les entiers symboliques (Int) et les vecteurs de bits (BitVec 4 bits). La comparaison montre que les BitVectors sont systématiquement plus rapides (2.3x à 6.4x), car leur domaine restreint (16 valeurs sur 4 bits) permet à Z3 d’utiliser des algorithmes de propagation plus efficaces. La contrainte Distinct, disponible nativement pour les entiers mais nécessitant une décomposition par paires pour les BitVectors, illustre le compromis entre simplicité d’API et performance. Au-delà du Sudoku, Z3 est un outil de résolution SMT polyvalent, applicable à la vérification de programmes, l’analyse de sécurité et la synthèse de code. Les exercices proposés (comptage de solutions, contraintes diagonales, coloration de graphe) montrent comment étendre le modèle de base vers des variantes plus riches.