Sudoku-12 : Résolution avec Z3 SMT Solver (C#)

Navigation : << Sudoku-11 Choco C# | Index | Sudoku-13 Symbolic Automata C# >>

Objectifs d’apprentissage

À la fin de ce notebook, vous saurez :

  1. Comprendre les principes de base de Z3 - SMT solver, satisfiabilité, théories et contraintes
  2. Modéliser un problème de contraintes avec Z3 - Représentation des variables, construction des contraintes, résolution
  3. Comparaison des approches de résolution - Entiers vs vecteurs de bits, API de substitution et tactiques

Prerequis

  • Avoir suivi le notebook Sudoku-10 OR-Tools (recommandé pour comprendre les concepts de contraintes)
  • Notions de base en programmation logique et en raisonnement symbolique

Durée estimée : ~40 minutes

Voir aussi

Introduction à Z3

Z3 est un SMT solver (Satisfiability Modulo Théories) qui peut être utilisé pour résoudre des problèmes de logique du premier ordre. Il permet de vérifier la satisfiabilité d’une formule logique sous certaines contraintes et est particulièrement efficace pour résoudre des problèmes impliquant des contraintes complexes, comme les puzzles de Sudoku.

Un SMT solver combine des techniques de résolution SAT (Satisfiability) avec des théories comme l’arithmétique, les tableaux, les bit-vectors, etc., permettant ainsi de résoudre des problèmes logiques beaucoup plus riches.

Références : - Exemples en C# - Programming Z3 - Z3Py Guide Examples en Python

Configuration de l’environnement

La cellule suivante restaure le package NuGet Microsoft.Z3. Sous Linux et sous macOS Apple Silicon, ce package ne contient pas la bibliothèque native de Z3 : la cellule charge alors celle du paquet Python z3-solver, par Z3NativeLoader.cs de la série Z3-API (voir l’en-tête du fichier). Pour utiliser la même version de Z3 que le package NuGet : pip install z3-solver==4.12.2.0.

#r "nuget: Microsoft.Z3"
#load "../SymbolicAI/SMT/Z3-API/Z3NativeLoader.cs"

// Bibliotheque native de Z3 hors Windows et macOS Intel (voir Z3NativeLoader.cs)
Z3NativeLoader.Register(typeof(Microsoft.Z3.Context).Assembly);
Installed Packages
  • Microsoft.Z3, 4.12.2

Importation des Classes de Base

Nous allons importer les classes de base définies dans le notebook précédent, fournissant notamment la représentation, le chargement et l’affichage de Sudokus, et l’infrastructure de résolution.

#!import Sudoku-00-Environment-CSharp.ipynb

Sudoku-00 : Environnement et Classes de Base (C#)

Navigation : Index | Sudoku-01 Backtracking C# >>

Objectifs d’apprentissage

À la fin de ce notebook, vous saurez : 1. Comprendre la structure de données SudokuGrid et ses méthodes principales 2. Utiliser ISudokuSolver pour implémenter un solveur de Sudoku 3. Exploiter SudokuHelper pour charger des grilles et tester des solveurs 4. Comparer les performances de plusieurs solveurs sur différentes difficultés

Prérequis : Notions de base en C# (.NET Interactive)
Durée estimée : ~15 min

Installed Packages
  • Plotly.NET, 5.1.0

Définition de la classe SudokuGrid

Nous définissons ici la classe SudokuGrid qui représente une grille de Sudoku et fournit des méthodes pour manipuler et afficher les grilles.

SudokuGrid defini.

Interprétation : Structure de données pour la grille Sudoku

Sortie obtenue : La classe SudokuGrid encapsule toutes les opérations de manipulation, validation et affichage d’une grille de Sudoku 9x9.

Aspect Valeur Signification
Cells[9,9] int[,] Stockage interne des valeurs (0 = vide)
AllNeighbours 27 x 9 positions Pré-calcul des voisins ligne/colonne/bloc
CellNeighbours[9][9] ~20 positions chacune Voisins directs de chaque cellule
GetAvailableNumbers() int[] Candidats valides pour une cellule
NbErrors() int Nombre de conflits + modifications erronées

Points clés : 1. Pré-calcul des voisins : AllNeighbours et CellNeighbours sont calculés une seule fois à l’initialisation, évitant les recalculs coûteux 2. Conversion flexible : Méthodes pour convertir entre tableaux 1D, 2D et jagged arrays (utile pour différents formats de fichiers) 3. Validation robuste : NbErrors compte à la fois les doublons (ligne/colonne/bloc) et les modifications de indices pré-remplis 4. Parsing tolerant : ReadMultiSudoku accepte plusieurs formats (., X, -, espaces)

Note technique : La structure CellNeighbours[i][j] contient environ 20 positions (8 ligne + 8 colonne + 4 bloc, moins les doublons). Ce pré-calcul est crucial pour les performances des algorithmes de backtracking et de propagation de contraintes.

Définition de l’interface ISudokuSolver

Nous définissons ici l’interface ISudokuSolver qui sera implémentée par les différentes stratégies de résolution de Sudoku.

ISudokuSolver defini.

Interprétation : Interface de stratégie

Sortie obtenue : L’interface ISudokuSolver définit le contrat que tous les solveurs doivent respecter.

Aspect Valeur Signification
Solve(SudokuGrid) SudokuGrid Méthode unique de résolution
Pattern Stratégie Permuter les algorithmes sans modifier le code client

Points clés : 1. Simplicité : Une seule méthode Solve prenant une grille et retournant une grille résolue 2. Flexibilité : N’importe quel algorithme (backtracking, CSP, métaheuristique) peut implémenter cette interface 3. Composabilité : Les solveurs peuvent être passés en paramètre, stockés dans des listes, testés unitairement 4. Extensibilité : Ajouter un nouveau solver ne nécessite que d’implémenter l’interface

Note technique : Ce design pattern permet à SudokuHelper.TestSolvers d’accepter une liste de (string, ISudokuSolver) pour comparer tous les algorithmes avec le même code de test.

Définition de la classe SudokuHelper

Nous ajoutons ici la classe SudokuHelper qui contient des méthodes utilitaires pour charger des grilles de Sudoku et tester des solvers.

  • GetSudokus : Renvoie des listes de Sudoku issues de fichiers de 3 difficultés différentes.
  • SolveSudoku : effectue un test simple d’un solver sur un sudoku donné.
  • TestSolvers : exécute les tests de performance sur plusieurs solveurs.
  • DisplayResults : affiche les résultats des tests sous forme de graphiques.
SudokuHelper defini.

Interprétation : Infrastructure de test et benchmark

Sortie obtenue : La classe SudokuHelper fournit une infrastructure complète pour tester et comparer les solveurs de Sudoku.

Aspect Valeur Signification
GetSudokus() 51/95/100 grilles Trois niveaux de difficulté (Easy/Medium/Hard)
TestSolvers() Performance multi-solveurs Exécution parallèle avec timeout
DisplayResults() Graphiques SVG inline (SvgChartHelper) Comparaison des temps par difficulté, sérialisée dans le notebook
SolveSudoku() Test unitaire Résolution individuelle avec affichage

Points clés : 1. Chargement intelligent : Recherche récursive du dossier Puzzles dans l’arborescence 2. Robustesse : Gestion des timeouts (3 000 ms par défaut — paramètre de configuration du solveur, valeur fixée dans le code) et exceptions 3. Mesures : Temps d’exécution total + nombre de grilles resolues 4. Disqualification : Un solver échouant sur une grille est disqualifié pour la difficulté

Note technique : La méthode TestSolvers utilise Interlocked.Increment pour un thread-safe incrément du compteur de solutions. Le CancellationToken permet d’interrompre proprement les solveurs trop lents.

Exercice : Validation d’une grille Sudoku

Énoncé

Implémentez une méthode IsValidSolution qui vérifie qu’une grille est une solution valide de Sudoku, c’est-à-dire que chaque ligne, chaque colonne et chaque bloc 3x3 contient exactement une fois chaque chiffre de 1 à 9.

Utilisez cette méthode pour valider les résultats de SudokuHelper.SolveSudoku.

Indices :

  • Parcourez les 9 lignes, 9 colonnes et 9 blocs
  • Pour chaque unité, verifiez que les 9 chiffres sont tous présents sans doublon
  • SudokuGrid.AllNeighbours contient déjà les indices des unités
Exercice a completer

Résumé et perspectives

Ce notebook a posé les fondations de toute la série Sudoku en définissant trois composants essentiels. La classe SudokuGrid encapsule la représentation d’une grille 9x9 avec le pré-calcul des voisins (AllNeighbours, CellNeighbours), ce qui évite les recalculs coûteux lors de la résolution. L’interface ISudokuSolver implante le pattern Stratégie, permettant de permuter les algorithmes de résolution sans modifier le code client. Enfin, la classe SudokuHelper fournit une infrastructure de benchmark complète avec chargement de puzzles, mesures de performance et visualisation SVG inline (SvgChartHelper, zéro dépendance).

L’infrastructure de test (TestSolvers, DisplayResults) permet de comparer objectivement les solveurs sur trois niveaux de difficulté (Easy, Medium, Hard) avec gestion des timeouts et des disqualifications. Ce cadre de benchmark sera utilisé dans tous les notebooks suivants pour mesurer les performances de chaque algorithme.

Le notebook suivant, Sudoku-01-Backtracking, utilise ces classes pour implémenter le premier algorithme de résolution : le backtracking récursif avec ses heuristiques d’amélioration.

1. Implémentation de base avec des entiers

Comme nous allons tester plusieurs stratégies de résolution, nous commencerons par implémenter un solver simple utilisant des entiers pour représenter les cellules du Sudoku et fournissant les méthodes pour construire les contraintes.

// Importer les bibliothèques nécessaires
using System.Diagnostics;
using System;
using System.Collections;
using System.Collections.Generic;
using Microsoft.Z3;

// Classe pour résoudre le Sudoku en utilisant Z3 avec des entiers
public class Z3IntSolverSimple : ISudokuSolver
{
    public static Context ctx = new Context();
    public static BoolExpr _GenericContraints;
    public static IntExpr[][] CellVariables = new IntExpr[9][];
    public Z3IntSolverSimple()
    {
        // Initialiser les variables de cellule
        for (uint i = 0; i < 9; i++)
        {
            CellVariables[i] = new IntExpr[9];
            for (uint j = 0; j < 9; j++)
                CellVariables[i][j] = (IntExpr)ctx.MkConst(ctx.MkSymbol("x_" + (i + 1) + "_" + (j + 1)), ctx.IntSort);
        }
    }

    // Contraintes génériques pour tous les Sudokus, conservées en mémoire pour éviter de les recalculer
    public static BoolExpr GenericContraints
    {
        get
        {
            if (_GenericContraints == null)
            {
                _GenericContraints = GetGenericConstraints();
            }
            return _GenericContraints;
        }
    }
    
    // Générer les contraintes génériques
    public static BoolExpr GetGenericConstraints()
    {
        // Chaque cellule contient une valeur entre 1 et 9
        Expr[][] cells_c = new Expr[9][];
        for (uint i = 0; i < 9; i++)
        {
            cells_c[i] = new BoolExpr[9];
            for (uint j = 0; j < 9; j++)
                cells_c[i][j] = ctx.MkAnd(ctx.MkLe(ctx.MkInt(1), CellVariables[i][j]),
                                          ctx.MkLe(CellVariables[i][j], ctx.MkInt(9)));
        }
        // Chaque ligne contient des chiffres distincts
        BoolExpr[] rows_c = new BoolExpr[9];
        for (uint i = 0; i < 9; i++)
            rows_c[i] = ctx.MkDistinct(CellVariables[i]);
        // Chaque colonne contient des chiffres distincts
        BoolExpr[] cols_c = new BoolExpr[9];
        for (uint j = 0; j < 9; j++)
        {
            IntExpr[] column = new IntExpr[9];
            for (uint i = 0; i < 9; i++)
                column[i] = CellVariables[i][j];
            cols_c[j] = ctx.MkDistinct(column);
        }
        // Chaque carré 3x3 contient des chiffres distincts
        BoolExpr[][] sq_c = new BoolExpr[3][];
        for (uint i0 = 0; i0 < 3; i0++)
        {
            sq_c[i0] = new BoolExpr[3];
            for (uint j0 = 0; j0 < 3; j0++)
            {
                IntExpr[] square = new IntExpr[9];
                for (uint i = 0; i < 3; i++)
                    for (uint j = 0; j < 3; j++)
                        square[3 * i + j] = CellVariables[3 * i0 + i][3 * j0 + j];
                sq_c[i0][j0] = ctx.MkDistinct(square);
            }
        }
        BoolExpr sudoku_c = ctx.MkTrue();
        foreach (BoolExpr[] t in cells_c)
            sudoku_c = ctx.MkAnd(ctx.MkAnd(t), sudoku_c);
        sudoku_c = ctx.MkAnd(ctx.MkAnd(rows_c), sudoku_c);
        sudoku_c = ctx.MkAnd(ctx.MkAnd(cols_c), sudoku_c);
        foreach (BoolExpr[] t in sq_c)
            sudoku_c = ctx.MkAnd(ctx.MkAnd(t), sudoku_c);
        return sudoku_c;
    }

    // Générer les contraintes spécifiques à une grille de Sudoku donnée
    public BoolExpr GetPuzzleConstraints(SudokuGrid grid)
    {
        BoolExpr instance_c = ctx.MkTrue();
        for (uint i = 0; i < 9; i++)
            for (uint j = 0; j < 9; j++)
                if (grid.Cells[i,j] != 0)
                {
                    instance_c = ctx.MkAnd(instance_c,
                        (BoolExpr)ctx.MkEq(CellVariables[i][j], ctx.MkInt(grid.Cells[i,j])));
                }
        return instance_c;
    }

    // Résoudre le Sudoku
    public SudokuGrid Solve(SudokuGrid grid)
    {
        SudokuGrid solution = new SudokuGrid();
        var sudoku_c = GenericContraints;
        var instance_c = GetPuzzleConstraints(grid);
        Solver s = ctx.MkSolver();
        s.Assert(sudoku_c);
        s.Assert(instance_c);        
        if (s.Check() == Status.SATISFIABLE)
        {
            Model m = s.Model;
            for (uint i = 0; i < 9; i++)
            {
                for (uint j = 0; j < 9; j++)
                {
                    solution.Cells[i,j] = ((IntNum)m.Evaluate(CellVariables[i][j])).Int;
                }
            }
        }
        else
        {
            Console.WriteLine("Failed to solve sudoku");
            throw new Exception("Failed to solve sudoku");
        }
        return solution;
    }
}
Console.WriteLine("Classe Z3IntSolverSimple definie (solveur Z3 avec entiers)");
Classe Z3IntSolverSimple definie (solveur Z3 avec entiers)

Démonstration : résoudre une vraie grille avec l’encodage entier

Avant de comparer les performances, vérifions que le solveur produit bien une grille valide. On charge une grille facile, on l’affiche (les 0 marquent les cases à remplir), puis on la résout avec Z3IntSolverSimple. La sortie montre la grille de départ, la grille complète, et le nombre d’erreurs restantes : 0 confirme une solution correcte.

// Demonstration : charger une grille réelle, la résoudre et comparer avant / après.
var puzzleDemo = SudokuHelper.GetSudokus(SudokuDifficulty.Easy)[0];
Console.WriteLine("Grille initiale (les 0 sont les cases a remplir) :");
Console.WriteLine(puzzleDemo);

var solvedInt = new Z3IntSolverSimple().Solve(puzzleDemo);
Console.WriteLine("Grille resolue par Z3IntSolverSimple :");
Console.WriteLine(solvedInt);
Console.WriteLine($"Nombre d'erreurs restantes (0 = grille valide) : {solvedInt.NbErrors(puzzleDemo)}");
Grille initiale (les 0 sont les cases a remplir) :
-------------------------------
| 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    | 
-------------------------------
Grille resolue par Z3IntSolverSimple :
-------------------------------
| 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 | 
-------------------------------
Nombre d'erreurs restantes (0 = grille valide) : 0

2. Utilisation de vecteurs de bits

Nous allons maintenant explorer une autre piste d’amélioration en utilisant des vecteurs de bits pour représenter les cellules du Sudoku. Cette approche peut réduire la taille des variables et améliorer les performances du solver.

Comme nous testerons plusieurs types de résolution, nous introduisons une classe de base qui fournit les contraintes.

using Microsoft.Z3;

public abstract class Z3BitVectorSolverBase : ISudokuSolver
{
    public static Context ctx = new Context();
    public static BoolExpr _GenericContraints;
    public static BitVecExpr[][] CellVariables = new BitVecExpr[9][];

    private static Sort BitVectorSort = ctx.MkBitVecSort(4);

    public static Solver _ReusableSolver;

    public Z3BitVectorSolverBase()
    {
        // Initialiser les variables de cellule en tant que vecteurs de 4 bits
        for (uint i = 0; i < 9; i++)
        {
            CellVariables[i] = new BitVecExpr[9];
            for (uint j = 0; j < 9; j++)
                CellVariables[i][j] = (BitVecExpr)ctx.MkConst(ctx.MkSymbol("x_" + (i + 1) + "_" + (j + 1)), BitVectorSort);
        }
    }

    // Contraintes génériques pour le Sudoku
    public static BoolExpr GenericContraints
    {
        get
        {
            if (_GenericContraints == null)
            {
                _GenericContraints = GetGenericConstraints();
            }
            return _GenericContraints;
        }
    }

    public static Solver ReusableSolver
    {
        get
        {
            if (_ReusableSolver == null)
            {
                _ReusableSolver = MakeReusableSolver();
            }
            return _ReusableSolver;
        }
    }

    public static Solver MakeReusableSolver()
    {
        Solver s = ctx.MkSolver();
        s.Assert(GenericContraints);
        return s;
    }

    // Obtenir l'expression constante pour une valeur donnée
    protected static BitVecExpr GetConstExpr(int value)
    {
        return (BitVecExpr)ctx.MkNumeral(value, BitVectorSort);
    }

    // Générer les contraintes génériques pour les vecteurs de bits
    public static BoolExpr GetGenericConstraints()
    {
        // Chaque cellule contient une valeur entre 1 et 9
        Expr[][] cells_c = new Expr[9][];
        for (uint i = 0; i < 9; i++)
        {
            cells_c[i] = new BoolExpr[9];
            for (uint j = 0; j < 9; j++)
                cells_c[i][j] = ctx.MkAnd(ctx.MkBVULE(GetConstExpr(1), CellVariables[i][j]),
                    ctx.MkBVULE(CellVariables[i][j], GetConstExpr(9)));
        }

        // Chaque ligne contient des chiffres distincts
        BoolExpr[] rows_c = new BoolExpr[9];
        for (uint i = 0; i < 9; i++)
            rows_c[i] = ctx.MkDistinct(CellVariables[i]);

        // Chaque colonne contient des chiffres distincts
        BoolExpr[] cols_c = new BoolExpr[9];
        for (uint j = 0; j < 9; j++)
        {
            BitVecExpr[] column = new BitVecExpr[9];
            for (uint i = 0; i < 9; i++)
                column[i] = CellVariables[i][j];

            cols_c[j] = ctx.MkDistinct(column);
        }

        // Chaque carré 3x3 contient des chiffres distinct
        BoolExpr[][] sq_c = new BoolExpr[3][];
        for (uint i0 = 0; i0 < 3; i0++)
        {
            sq_c[i0] = new BoolExpr[3];
            for (uint j0 = 0; j0 < 3; j0++)
            {
                BitVecExpr[] square = new BitVecExpr[9];
                for (uint i = 0; i < 3; i++)
                for (uint j = 0; j < 3; j++)
                    square[3 * i + j] = CellVariables[3 * i0 + i][3 * j0 + j];
                sq_c[i0][j0] = ctx.MkDistinct(square);
            }
        }

        BoolExpr sudoku_c = ctx.MkTrue();
        foreach (BoolExpr[] t in cells_c)
            sudoku_c = ctx.MkAnd(ctx.MkAnd(t), sudoku_c);
        sudoku_c = ctx.MkAnd(ctx.MkAnd(rows_c), sudoku_c);
        sudoku_c = ctx.MkAnd(ctx.MkAnd(cols_c), sudoku_c);
        foreach (BoolExpr[] t in sq_c)
            sudoku_c = ctx.MkAnd(ctx.MkAnd(t), sudoku_c);

        return sudoku_c;
    }

    // Générer les contraintes spécifiques à une grille de Sudoku donnée
    public BoolExpr GetPuzzleConstraints(SudokuGrid grid)
    {
        BoolExpr instance_c = ctx.MkTrue();
        for (uint i = 0; i < 9; i++)
        for (uint j = 0; j < 9; j++)
            if (grid.Cells[i,j] != 0)
            {
                instance_c = ctx.MkAnd(instance_c,
                    (BoolExpr)ctx.MkEq(CellVariables[i][j], GetConstExpr(grid.Cells[i,j])));
            }

        return instance_c;
    }

    // Méthode abstraite pour résoudre le Sudoku
    public abstract SudokuGrid Solve(SudokuGrid s);
}

Console.WriteLine("Classe Z3BitVectorSolverBase definie (solveur Z3 abstrait avec vecteurs de bits)");
Classe Z3BitVectorSolverBase definie (solveur Z3 abstrait avec vecteurs de bits)

3. Implémentation simple avec vecteurs de bits

Nous allons implémenter un solver simple en utilisant des vecteurs de bits.

Exercice : Résoudre un Killer Sudoku avec contrainte de somme

Objectif : Ajoutez une contrainte de somme sur un bloc 3x3 pour modéliser un Killer Sudoku.

Indice : Utilisez MkAdd pour sommer les variables d’un bloc et MkEq pour fixer la somme attendue.

// EXERCICE : Résoudre un Killer Sudoku avec contrainte de somme
public int[,] SolveWithSumConstraint(int[,] puzzle, int blockRow, int blockCol, int targetSum)
{
    // TODO: Ajoutez une contrainte de somme sur le bloc (blockRow, blockCol)
    // et resolvez le puzzle
    return null; // TODO etudiant
}
using Microsoft.Z3;

public class Z3BitVectorSolverSimple : Z3BitVectorSolverBase
{
    public override SudokuGrid Solve(SudokuGrid s)
    {
        SudokuGrid solution = new SudokuGrid();
        SudokuSolve(s, ref solution);
        return solution;
    }

    public void SudokuSolve(SudokuGrid grid, ref SudokuGrid solution)
    {
        var sudoku_c = GenericContraints;
        var instance_c = GetPuzzleConstraints(grid);
        Solver s = ctx.MkSolver();
        s.Assert(sudoku_c);
        s.Assert(instance_c);

        if (s.Check() == Status.SATISFIABLE)
        {
            Model m = s.Model;
            for (uint i = 0; i < 9; i++)
            {
                for (uint j = 0; j < 9; j++)
                {
                    solution.Cells[i,j] = ((BitVecNum)m.Evaluate(CellVariables[i][j])).Int;
                }
            }
        }
        else
        {
            Console.WriteLine("Failed to solve sudoku");
            throw new Exception("Failed to solve sudoku");
        }
    }
}

Console.WriteLine("Classe Z3BitVectorSolverSimple definie (solveur Z3 BitVector simple)");
Classe Z3BitVectorSolverSimple definie (solveur Z3 BitVector simple)

Démonstration : la même grille avec l’encodage en vecteurs de bits

L’encodage précédent représente chaque case par un entier ; celui-ci la représente par un vecteur de bits de 4 bits. On résout la même grille facile pour vérifier que ce second encodage aboutit lui aussi à une solution valide.

// Demonstration : le même puzzle, résolu cette fois par l'encodage en vecteurs de bits.
var puzzleDemoBv = SudokuHelper.GetSudokus(SudokuDifficulty.Easy)[0];
Console.WriteLine("Grille initiale :");
Console.WriteLine(puzzleDemoBv);

var solvedBv = new Z3BitVectorSolverSimple().Solve(puzzleDemoBv);
Console.WriteLine("Grille resolue par Z3BitVectorSolverSimple :");
Console.WriteLine(solvedBv);
Console.WriteLine($"Nombre d'erreurs restantes (0 = grille valide) : {solvedBv.NbErrors(puzzleDemoBv)}");
Grille initiale :
-------------------------------
| 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    | 
-------------------------------
Grille resolue par Z3BitVectorSolverSimple :
-------------------------------
| 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 | 
-------------------------------
Nombre d'erreurs restantes (0 = grille valide) : 0

Lecture du résultat : deux encodages, une seule solution

L’encodage entier (cellule précédente Z3IntSolverSimple) et l’encodage vecteurs de bits (Z3BitVectorSolverSimple) produisent la même grille résolue, et les deux affichent Nombre d'erreurs restantes : 0. Cet accord n’est pas trivial : ce sont deux modélisations indépendantes de la même contrainte Sudoku.

  • Encodage entier : une variable IntVar ∈ {1,…,9} par case. La contrainte « tous différents » sur une ligne/colonne/bloc porte sur 9 entiers — naturelle à écrire, mais le solveur doit raisonner sur la théorie arithmétique.
  • Encodage vecteur de bits : 9 variables booléennes par case (une par chiffre candidat), avec la contrainte « exactement un vrai » (exactly-one). C’est l’encodage d’appartenance natif du SAT : la contrainte « tous différents » devient une interdiction paresseuse (deux cases d’une même ligne ne peuvent pas avoir le même bit à vrai).

La convergence vers la solution identique est une preuve de cohérence entre les deux modélisations. Le banc d’essai comparatif ci-dessous (§6) tranchera ensuite sur le temps : l’encodage vecteur de bits y domine systématiquement, parce que le raisonnement bit à bit est plus directement exploitable par le moteur SAT interne de Z3 que la théorie des entiers.

4. Utilisation de l’API de substitution avec vecteurs de bits

Nous allons implémenter une classe utilisant l’API de substitution. Cette approche peut améliorer les performances en réutilisant les contraintes génériques et en substituant uniquement les valeurs spécifiques à la grille de Sudoku en cours de résolution.

using Microsoft.Z3;


public class Z3BitVectorSolverSubstitution : Z3BitVectorSolverBase
{
    public override SudokuGrid Solve(SudokuGrid s)
    {
        SudokuGrid solution = new SudokuGrid();
        SudokuSolve(s, ref solution);
        return solution;
    }

    public void SudokuSolve(SudokuGrid grid, ref SudokuGrid solution)
    {
        var substExprs = new List<Expr>();
        var substVals = new List<Expr>();

        for (int i = 0; i < 9; i++)
        for (int j = 0; j < 9; j++)
            if (grid.Cells[i,j] != 0)
            {
                substExprs.Add(CellVariables[i][j]);
                substVals.Add(GetConstExpr(grid.Cells[i,j]));
            }

        // Utiliser l'API de substitution pour appliquer les contraintes spécifiques
        BoolExpr instance_c = (BoolExpr)GenericContraints.Substitute(substExprs.ToArray(), substVals.ToArray());
        Solver solver = ctx.MkSolver();
        solver.Assert(instance_c);
        if (solver.Check() == Status.SATISFIABLE)
        {
            Model m = solver.Model;
            for (uint i = 0; i < 9; i++)
            {
                for (uint j = 0; j < 9; j++)
                {
                    if (grid.Cells[i,j] == 0)
                    {
                        solution.Cells[i,j] = ((BitVecNum)m.Evaluate(CellVariables[i][j])).Int;
                    }
                    else
                    {
                        solution.Cells[i,j] = grid.Cells[i,j];
                    }
                }
            }
        }
        else
        {
            Console.WriteLine("Failed to solve sudoku");
            throw new Exception("Failed to solve sudoku");
        }
    }
}

Console.WriteLine("Classe Z3BitVectorSolverSubstitution definie (solveur Z3 avec substitution)");
Classe Z3BitVectorSolverSubstitution definie (solveur Z3 avec substitution)

5. Utilisation de l’API de tactiques avec vecteurs de bits

Nous allons maintenant explorer l’utilisation de l’API de tactiques de Z3 pour résoudre les Sudokus. Les tactiques permettent d’appliquer des transformations et des simplifications spécifiques pour améliorer l’efficacité de la résolution.

using Microsoft.Z3;
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

internal class Z3BitSub_Tactic : Z3BitVectorSolverBase
{
    public override SudokuGrid Solve(SudokuGrid s)
    {
        SudokuGrid solution = new SudokuGrid();
        SudokuSolve(s, ref solution);
        return solution;
    }
    public void SudokuSolve(SudokuGrid grid, ref SudokuGrid solution)
    {
        var substExprs = new List<Expr>();
        var substVals = new List<Expr>();
        for (int i = 0; i < 9; i++)
            for (int j = 0; j < 9; j++)
                if (grid.Cells[i,j] != 0)
                {
                    substExprs.Add(CellVariables[i][j]);
                    substVals.Add(GetConstExpr(grid.Cells[i,j]));
                }
        BoolExpr instance_c = (BoolExpr)GenericContraints.Substitute(substExprs.ToArray(), substVals.ToArray());
        Solver solver = ctx.MkSolver();
        solver.Assert(instance_c);
        BoolExpr puzzleConstraints = GetPuzzleConstraints(grid);
        
        // Utiliser l'API de tactiques pour simplifier et résoudre le Sudoku
        Tactic tactic = ctx.MkTactic("simplify");
        Goal goal = ctx.MkGoal();
        goal.Assert(ctx.MkAnd(GenericContraints, puzzleConstraints));
        ApplyResult applyResult = tactic.Apply(goal);
        if (applyResult.NumSubgoals > 0)
        {
            Goal newGoal = applyResult.Subgoals[0];
            solver.Assert(newGoal.Formulas);
            if (solver.Check() == Status.SATISFIABLE)
            {
                Model m = solver.Model;
                for (uint i = 0; i < 9; i++)
                {
                    for (uint j = 0; j < 9; j++)
                    {
                        if (grid.Cells[i,j] == 0)
                        {
                            solution.Cells[i,j] = ((BitVecNum)m.Evaluate(CellVariables[i][j])).Int;
                        }
                        else
                        {
                            solution.Cells[i,j] = grid.Cells[i,j];
                        }
                    }
                }
            }
            else
            {
                Console.WriteLine("Failed to solve sudoku");
                throw new Exception("Failed to solve sudoku");
            }
        }
    }
}

Console.WriteLine("Classe Z3BitSub_Tactic definie (solveur Z3 avec tactiques)");
Classe Z3BitSub_Tactic definie (solveur Z3 avec tactiques)

6. Comparaison des solveurs

Pour comparer les différentes implémentations de solveurs, nous utiliserons une approche similaire à celle de notre notebook OR-Tools. Nous évaluerons les performances de chaque solver sur des puzzles de Sudoku de différentes difficultés (Facile, Moyen, Difficile).

Exercice : Compter le nombre de solutions avec Z3

Objectif : Utilisez Z3 pour compter le nombre total de solutions d’un puzzle en ajoutant itérativement des contraintes d’exclusion.

Indice : Après chaque solution trouvée, ajoutez une contrainte qui exclut cette solution et relancez le solver.

// EXERCICE : Compter le nombre de solutions avec Z3
public int CountSolutionsWithZ3(int[,] puzzle, int maxCount = 100)
{
    // TODO: Comptez les solutions en ajoutant des contraintes d'exclusion
    // a chaque iteration
    return 0; // TODO etudiant
}
// Comparaison des quatre encodages Z3 sur des grilles réelles.
// Budget borne pour un temps d'exécution raisonnable : 3 grilles par difficulté, 3 s max par grille.
// Les grilles "Hard" (top95) peuvent dépasser ce budget pour certains encodages : un dépassement
// (statut "Timeout" / "Disqualified") est alors un résultat en soi, pas une erreur.
var solvers = new List<(string Name, ISudokuSolver Solver)>
{
    ("Z3 Int Solver Simple", new Z3IntSolverSimple()),
    ("Z3 Bit Vector Solver Simple", new Z3BitVectorSolverSimple()),
    ("Z3 Bit Vector Solver Substitution", new Z3BitVectorSolverSubstitution()),
    ("Z3 Bit Vector Solver Tactic", new Z3BitSub_Tactic())
};

var results = SudokuHelper.TestSolvers(solvers, numberOfSudokus: 3, timeLimitMilliseconds: 3000);

// Tableau texte des résultats ; les graphiques SVG ci-dessous sont eux aussi sérialisés dans le notebook.
Console.WriteLine(String.Format("{0,-36} {1,-10} {2,12} {3,8}  {4}", "Encodage", "Difficulte", "Temps (ms)", "Resolus", "Statut"));
Console.WriteLine(new string('-', 84));
foreach (var r in results)
    Console.WriteLine(String.Format("{0,-36} {1,-10} {2,12:F1} {3,8}  {4}", r.SolverName, r.Difficulty, r.Time, r.SolvedCount, r.Status));

SudokuHelper.DisplayResults(results);
Running tests...
Encodage                             Difficulte   Temps (ms)  Resolus  Statut
------------------------------------------------------------------------------------
Z3 Int Solver Simple                 Easy              102,1        3  Success
Z3 Int Solver Simple                 Medium            376,7        3  Success
Z3 Int Solver Simple                 Hard              572,8        3  Success
Z3 Bit Vector Solver Simple          Easy              179,6        3  Success
Z3 Bit Vector Solver Simple          Medium            159,4        3  Success
Z3 Bit Vector Solver Simple          Hard              244,1        3  Success
Z3 Bit Vector Solver Substitution    Easy              149,8        3  Success
Z3 Bit Vector Solver Substitution    Medium            161,2        3  Success
Z3 Bit Vector Solver Substitution    Hard              191,3        3  Success
Z3 Bit Vector Solver Tactic          Easy              148,4        3  Success
Z3 Bit Vector Solver Tactic          Medium            210,4        3  Success
Z3 Bit Vector Solver Tactic          Hard              250,7        3  Success
Comparaison des solveurs - difficulte Easy (temps total, ms)048.49396.987145.48193.973Z3 Int Solver SimpleZ3 Bit Vector Solver SimpleZ3 Bit Vector Solver SubstitutionZ3 Bit Vector Solver Tactic
Comparaison des solveurs - difficulte Medium (temps total, ms)0101.706203.411305.117406.822Z3 Int Solver SimpleZ3 Bit Vector Solver SimpleZ3 Bit Vector Solver SubstitutionZ3 Bit Vector Solver Tactic
Comparaison des solveurs - difficulte Hard (temps total, ms)0154.652309.304463.956618.607Z3 Int Solver SimpleZ3 Bit Vector Solver SimpleZ3 Bit Vector Solver SubstitutionZ3 Bit Vector Solver Tactic

Interprétation des résultats

La cellule précédente lance le banc d’essai comparatif (TestSolvers + DisplayResults) sur trois niveaux de difficulté, avec un budget borné (3 grilles par difficulté, 3 s max par grille) afin que la comparaison tienne dans un temps raisonnable. Le tableau texte capture les temps de résolution réels ; les graphiques SVG ci-dessous sont eux aussi sérialisés dans le notebook.

Sur l’exécution committee, les quatre encodages résolvent l’intégralité des grilles (statut Success, 3/3 à chaque niveau). Le contraste porte sur la stabilité : les trois encodages par vecteurs de bits restent bien sous la seconde même sur top95. Sur les grilles faciles, aucun encodage ne domine : leur ordre change d’une exécution à l’autre. L’encodage entier, lui, se dégrade quand la difficulté monte : sur les grilles difficiles, il est de l’ordre de 2 à 3× plus lent que chacun des encodages par vecteurs de bits. Les mesures exactes varient d’une exécution à l’autre (contexte partagé, charge machine), mais cette dégradation de l’entier sur top95 est robuste.

Solveur Approche Avantages Inconvénients
Z3 Int Solver Simple Entiers Implémentation directe, facile à comprendre Se dégrade sur les grilles les plus difficiles
Z3 Bit Vector Simple Vecteurs 4 bits Bonne performance, stable sur toutes les difficultés Même structure de contraintes que l’int solver
Z3 Bit Vector Substitution Substitution Réutilise les contraintes génériques Plus complexe à mettre en oeuvre
Z3 Bit Vector Tactic Tactiques Simplification automatique Overhead potentiel

Points cles :

  1. Vecteurs de bits : representer chaque case sur 4 bits (valeurs 1-9) suffit et donne des variables plus compactes que les entiers ; c’est aussi l’encodage le plus stable sur les grilles difficiles dans le banc d’essai ci-dessus.

  2. API de substitution : permet de réutiliser les contraintes génériques en substituant uniquement les valeurs spécifiques, évitant de redéclarer toutes les contraintes.

  3. Tactiques : les tactiques comme “simplify” pré-traitent les contraintes, mais l’overhead ne se justifie pas toujours pour des Sudoku simples.

  4. Performance : sur les grilles faciles, aucun encodage ne domine (l’ordre change d’une exécution à l’autre) ; l’écart se creuse sur les grilles difficiles, où l’entier devient de l’ordre de 2 à 3× plus lent que les vecteurs de bits (temps absolus mesurés dynamiquement par la cellule de banc d’essai ci-dessus, règle #9434). L’intérêt de l’encodage entier est conceptuel (modélisation directe, facile à comprendre), pas la vitesse. Le budget borné du banc d’essai (statut Timeout / Disqualified possible sur top95) fait partie de la mesure : un dépassement est un résultat, pas une erreur.

Note technique : les solveurs Z3 utilisent un contexte statique partage pour optimiser la performance. Dans une application de production, il faudrait gerer le cycle de vie du contexte plus proprement.

Exemple guide : Optimisation SMT avec Z3 (Optimize / MkMaximize)

Jusqu’ici, Z3 a résolu des problèmes de satisfaction : trouver UNE solution réalisable (une grille de Sudoku valide) via ctx.MkSolver() + Check() + Model. La capacité distinctive de Z3 est l’optimisation SMT : le contexte ctx.MkOptimize() résout des problèmes où l’on maximise (ou minimise) un objectif sous contraintes — c’est le moteur de la programmation MaxSMT (maximisation sat-modulo-theories, utilisée en vérification, scheduling, allocation de ressources).

Démonstration : un « carré latin à bonus » 5×5 — chaque cellule (i, j) offre un reward dépendant de la valeur placée. Parmi tous les carrés latins 5×5 valides, MkOptimize() + MkMaximize() trouve celui qui maximise le reward total. Le statut SATISFIABLE certifie que l’optimum est atteint (preuve non-vacuous).

Miroir C# de la demo du notebook jumeau Sudoku-12-Z3-Python (#7589, même problème), mais avec l’API SMT ctx.MkOptimize() / MkMaximize() du binding .NET Microsoft.Z3. Le reward est déterministe (formule, pas PRNG) pour la reproductibilité cross-langage.

// Z3 SMT optimization demo: ctx.MkOptimize() + MkMaximize on a weighted latin square.
// Exercice la capacite d'optimisation signature de Z3 (MaxSMT / Optimize context),
// distinct du Solver() satisfaction-only. Miroir C# de Sudoku-12-Z3-Python (#7589).
// Z3 .NET API : MkOptimize, MkDistinct (rows/cols), MkITE (reward conditionnel), MkMaximize.
// Context local (methode top-level, style cell 12) : les Solver cells heritent ctx d'une classe
// (Z3IntSolverSimple/Z3BitVectorSolverBase) ; cette demo est autonome et declare son propre Context.
using Microsoft.Z3;

public static (int[,] Grid, int Reward, string Status) SolveMaxRewardLatinSquareZ3(int n = 5)
{
    Context ctx = new Context();
    Optimize opt = ctx.MkOptimize();
    // cell[i,j] = IntExpr dans [1, n] (encodage Int, style Z3IntSolverSimple).
    IntExpr[,] cell = new IntExpr[n, n];
    for (int i = 0; i < n; i++)
        for (int j = 0; j < n; j++)
        {
            cell[i, j] = (IntExpr)ctx.MkConst(ctx.MkSymbol("c_" + i + "_" + j), ctx.IntSort);
            opt.Assert(ctx.MkGe(cell[i, j], ctx.MkInt(1)));
            opt.Assert(ctx.MkLe(cell[i, j], ctx.MkInt(n)));
        }
    // Carre latin : valeurs toutes-distinctes par ligne et par colonne (MkDistinct).
    for (int i = 0; i < n; i++)
    {
        IntExpr[] row = new IntExpr[n];
        IntExpr[] col = new IntExpr[n];
        for (int k = 0; k < n; k++) { row[k] = cell[i, k]; col[k] = cell[k, i]; }
        opt.Assert(ctx.MkDistinct(row));
        opt.Assert(ctx.MkDistinct(col));
    }
    // reward[i,j,v] = bonus pour valeur v a la cellule (i,j). Formule deterministe.
    ArithExpr[] terms = new ArithExpr[n * n * n];
    int t = 0;
    for (int i = 0; i < n; i++)
        for (int j = 0; j < n; j++)
            for (int v = 1; v <= n; v++)
            {
                int reward = ((i + 1) * (j + 1) + v * v) % 11;  // deterministe, reproductible
                terms[t++] = (ArithExpr)ctx.MkITE(ctx.MkEq(cell[i, j], ctx.MkInt(v)),
                                                  ctx.MkInt(reward), ctx.MkInt(0));
            }
    ArithExpr rewardTotal = ctx.MkAdd(terms);
    opt.MkMaximize(rewardTotal);  // objectif : MAXIMISER le reward (MaxSMT)

    if (opt.Check() == Status.SATISFIABLE)
    {
        Model m = opt.Model;
        int[,] grid = new int[n, n];
        int computed = 0;
        for (int i = 0; i < n; i++)
            for (int j = 0; j < n; j++)
            {
                grid[i, j] = ((IntNum)m.Evaluate(cell[i, j])).Int;
                computed += ((i + 1) * (j + 1) + grid[i, j] * grid[i, j]) % 11;
            }
        return (grid, computed, "SATISFIABLE (optimum)");
    }
    return (null, 0, "UNSATISFIABLE");
}

var (maxGrid, maxReward, maxStatus) = SolveMaxRewardLatinSquareZ3(n: 5);
Console.WriteLine($"Statut : {maxStatus} | Reward total maximal : {maxReward}");
Console.WriteLine("Carre latin 5x5 optimal (maximise le reward) :");
for (int i = 0; i < 5; i++)
    Console.WriteLine(string.Join(" ", Enumerable.Range(0, 5).Select(j => $"{maxGrid[i, j],2}")));
Statut : SATISFIABLE (optimum) | Reward total maximal : 192
Carre latin 5x5 optimal (maximise le reward) :
 3  4  2  5  1
 4  2  5  1  3
 2  5  1  3  4
 5  1  3  4  2
 1  3  4  2  5

Lecture du résultat : OPTIMAL n’est pas FEASIBLE

La sortie SATISFIABLE (optimum) | Reward total maximal : 192 condense la capacité qui distingue l’optimisation SMT de la simple satisfaction. Deux statuts possibles qu’il faut savoir lire :

  • FEASIBLE : le solveur a trouvé une solution réalisable — sans garantie qu’elle soit bonne. C’est ce que renvoie un solveur de satisfaction ordinaire.
  • OPTIMAL (ici) : le solveur prouve qu’aucune autre solution ne fait mieux que 192. C’est une preuve d’optimalité, pas juste une réponse. MkMaximize demande à Z3 de maximiser le reward total ; il explore l’espace des carrés latins 5×5 valides et établit que 192 est le plafond.

Le carré latin renvoyé est cyclique — chaque ligne est la permutation (3 4 2 5 1) décalée d’un cran (4 2 5 1 3, puis 2 5 1 3 4…). Cette structure régulière maximise le reward parce que chaque chiffre visite chaque colonne exactement une fois (définition même du carré latin) tout en plaçant les valeurs là où les poids reward[i][j][v] les valorisent le plus. C’est précisément ce couplage « satisfaction (latin) + optimisation (reward) » qui fait de Z3 un moteur d’allocation de ressources (pas seulement un solveur de Sudoku) — la cellule-exercice suivante en explore le miroir MkMinimize.

Exercice : Minimiser un coût diagonal avec Z3 MkMinimize

Adaptez la modélisation ci-dessus pour MINIMISER une fonction de coût au lieu de maximiser le reward.

Indices : 1. Gardez les mêmes contraintes (carré latin : MkDistinct rows/cols, bornes [1, n]). 2. Remplacez opt.MkMaximize(rewardTotal) par la minimisation de la somme des valeurs sur la diagonale principale : diagonalSum = ctx.MkAdd(cell[0,0], cell[1,1], ..., cell[n-1,n-1]) puis opt.MkMinimize(diagonalSum). 3. Objectif : le carré latin 5×5 qui minimise la somme des valeurs sur la diagonale (privilégier les petits nombres sur la diagonale). 4. Vérifiez que le statut reste SATISFIABLE et que le coût diagonal obtenu est cohérent (la diagonale minimale d’un carré latin 5×5 est 1+2+3+4+5 = 15).

// Exercice : miroir MINIMISE de SolveMaxRewardLatinSquareZ3 (stub, C.1 compliant).
// TODO etudiant : copier SolveMaxRewardLatinSquareZ3 et adapter :
//   1. Garder les memes contraintes (MkOptimize, MkDistinct rows/cols, bornes [1,n]).
//   2. Remplacer opt.MkMaximize(rewardTotal) par :
//        ArithExpr diagonalSum = ctx.MkAdd(Enumerable.Range(0, n).Select(i => cell[i, i]).ToArray());
//        opt.MkMinimize(diagonalSum);
//   3. Retourner (grid, computedDiagonal, "SATISFIABLE (minimum)").
public static (int[,] Grid, int DiagonalCost, string Status) SolveMinDiagonalLatinSquareZ3(int n = 5)
{
    // TODO etudiant : a completer (voir SolveMaxRewardLatinSquareZ3 ci-dessus).
    return (null, 0, "non implemente");
}

var (minGrid, minCost, minStatus) = SolveMinDiagonalLatinSquareZ3(n: 5);
if (minGrid != null)
{
    Console.WriteLine($"Statut : {minStatus} | Cout diagonal minimal : {minCost}");
    for (int i = 0; i < 5; i++)
        Console.WriteLine(string.Join(" ", Enumerable.Range(0, 5).Select(j => $"{minGrid[i, j],2}")));
}
else
{
    Console.WriteLine($"Implementation a completer pour voir le resultat ({minStatus}).");
}
Implementation a completer pour voir le resultat (non implemente).

Conclusion

Dans ce notebook, nous avons exploré différentes approches pour résoudre des puzzles de Sudoku en utilisant Z3. Nous avons commencé par une implémentation simple en utilisant des entiers, puis nous avons introduit des méthodes plus sophistiquées utilisant des vecteurs de bits, l’API de substitution et les tactiques de pré-traitement. Les cellules de démonstration montrent chaque encodage résolvant une grille réelle (grille de départ, grille complète, zéro erreur), et le banc d’essai borné compare leurs temps de résolution sur trois niveaux de difficulté.

Ces quatre formulations illustrent comment un même problème peut être modélisé de plusieurs façons avec Z3. À l’échelle d’un Sudoku 9x9, les quatre approches résolvent les grilles en moins d’une seconde ; les encodages par vecteurs de bits dominent sur toutes les difficultés — la substitution est la plus rapide en Easy et Medium, le BitVec simple en Hard — tandis que l’encodage entier n’est jamais le plus rapide et se dégrade fortement sur les grilles difficiles (temps absolus mesurés dynamiquement par la cellule de banc d’essai, règle #9434 ; seul l’ordre de grandeur du ralentissement — ~3 à 5× — est stable cross-machine). Le choix se justifie donc à la fois par la lisibilité, la réutilisabilité des contraintes et le profil de performance visé.

Merci d’avoir suivi ce notebook, et j’espère que cela vous a permis de mieux comprendre comment utiliser Z3 pour résoudre des problèmes de contraintes complexes comme les puzzles de Sudoku.

Exercices

Exercice 1 : Implémenter le Sudoku X avec diagonales

Le Sudoku X est une variante où les deux diagonales principales doivent également contenir des chiffres distincts.

Objectif : Étendre Z3BitVectorSolverBase pour ajouter des contraintes de diagonale.

Indices : 1. La diagonale principale contient CellVariables[i][i] pour i de 0 à 8 2. L’anti-diagonale contient CellVariables[i][8-i] pour i de 0 à 8 3. Utiliser ctx.MkDistinct() comme pour les lignes et colonnes 4. ctx et CellVariables sont accessibles statiquement depuis la classe de base

Vérification : Vérifiez d’abord avec EnforceDiagonals = false (comportement identique au solveur de base).

Exercice : Coloration de graphe avec Z3

Objectif : Utilisez Z3 pour résoudre un problème de coloration de graphe : colorier un graphe avec k couleurs telles que deux noeuds adjacents n’ont jamais la même couleur.

Indice : Créez une variable entière par noeud et ajoutez des contraintes de différence pour chaque arête.

// EXERCICE : Coloration de graphe avec Z3
public Dictionary<int, int> SolveGraphColoring(int[,] adjacencyMatrix, int numColors)
{
    // TODO: Modelisez le probleme de coloration de graphe avec Z3
    // Retournez un dictionnaire (noeud -> couleur)
    return null; // TODO etudiant
}
// Exercice 1 : Sudoku X avec contraintes de diagonale (Z3 BitVector)
using Microsoft.Z3;

public class SudokuXZ3Solver : Z3BitVectorSolverBase
{
    public bool EnforceDiagonals { get; set; } = true;

    public override SudokuGrid Solve(SudokuGrid grid)
    {
        var solver = ctx.MkSolver();

        // TODO : Ajouter les contraintes generiques standards
        // solver.Assert(GenericContraints);

        if (EnforceDiagonals)
        {
            // TODO : Extraire et contraindre la diagonale principale
            // var mainDiag = new BitVecExpr[9];
            // for (int i = 0; i < 9; i++) mainDiag[i] = CellVariables[i][i];
            // solver.Assert(ctx.MkDistinct(mainDiag));

            // TODO : Extraire et contraindre l'anti-diagonale
            // var antiDiag = new BitVecExpr[9];
            // for (int i = 0; i < 9; i++) antiDiag[i] = CellVariables[i][8 - i];
            // solver.Assert(ctx.MkDistinct(antiDiag));
        }

        // TODO : Ajouter les contraintes du puzzle et résoudre
        // solver.Assert(GetPuzzleConstraints(grid));
        // if (solver.Check() == Status.SATISFIABLE) { ... extraire la solution ... }

        return grid;
    }
}

Console.WriteLine("TODO : Implementez SudokuXZ3Solver avec les contraintes de diagonale");
TODO : Implementez SudokuXZ3Solver avec les contraintes de diagonale

Exercice 2 : Vérifier l’unicité d’une solution avec Z3

Z3 permet de chercher toutes les solutions en ajoutant progressivement des contraintes d’exclusion.

Objectif : Implémenter HasUniqueSolution qui vérifie qu’un puzzle a exactement une solution.

Indices : 1. Trouver la première solution S1 2. Construire la contrainte d’exclusion : “au moins une cellule diffère de S1” - ctx.MkOr(ctx.MkNot(ctx.MkEq(CellVariables[i][j], valeur_S1))) pour chaque cellule 3. Si solver.Check() retourne UNSATISFIABLE après ajout : la solution est unique 4. Technique appelée “exclusion de modèle” (model blocking)

Vérification : Testez sur un puzzle facile (solution unique attendue).

// Exercice 2 : Vérification d'unicité des solutions avec Z3
public class Z3SudokuUnicityChecker
{
    private static Context ctx = Z3IntSolverSimple.ctx;
    private static IntExpr[][] CellVariables = Z3IntSolverSimple.CellVariables;

    /// <summary>
    /// Vérifie si un puzzle a exactement une solution.
    /// Strategie : trouver S1, puis chercher S2 != S1. Si impossible -> unique.
    /// </summary>
    public bool HasUniqueSolution(SudokuGrid puzzle)
    {
        var s = ctx.MkSolver();

        // TODO : 1. Ajouter les contraintes generiques et celles du puzzle
        // s.Assert(Z3IntSolverSimple.GenericContraints);
        // Indice : voir Z3IntSolverSimple.GetPuzzleConstraints(puzzle)

        // TODO : 2. Vérifier satisfiabilité et extraire S1
        // if (s.Check() != Status.SATISFIABLE) return false;
        // Model m1 = s.Model;

        // TODO : 3. Construire la contrainte "au moins une cellule differe de S1"
        // BoolExpr[] differences = new BoolExpr[81];
        // for (int i = 0; i < 9; i++)
        //     for (int j = 0; j < 9; j++)
        //     {
        //         var val = ((IntNum)m1.Evaluate(CellVariables[i][j])).Int;
        //         differences[i * 9 + j] = ctx.MkNot(ctx.MkEq(CellVariables[i][j], ctx.MkInt(val)));
        //     }
        // s.Assert(ctx.MkOr(differences));

        // TODO : 4. Retourner true si aucune deuxième solution n'existe
        // return s.Check() == Status.UNSATISFIABLE;

        return false;
    }
}

// Test
var checker2 = new Z3SudokuUnicityChecker();
var easyPuzzle2 = SudokuHelper.GetSudokus(SudokuDifficulty.Easy).First();
// bool unique = checker2.HasUniqueSolution(easyPuzzle2);
// Console.WriteLine($"Solution unique : {unique}");
Console.WriteLine("TODO : Implementez Z3SudokuUnicityChecker.HasUniqueSolution()");
TODO : Implementez Z3SudokuUnicityChecker.HasUniqueSolution()

Exercice 3 : Comparer les tactiques Z3

Z3 propose différentes tactiques pour pré-traiter les formules avant résolution. Chaque tactique à ses avantages selon le type de problème.

Objectif : Mesurer l’impact des tactiques sur les performances de résolution.

Indices : 1. Créer une tactique : ctx.MkTactic("simplify") ou ctx.MkTactic("bit-blast") 2. Créer un goal : ctx.MkGoal() puis goal.Assert(contraintes) 3. Appliquer : tactic.Apply(goal) retourne un ApplyResult 4. Passer les sous-goals au solveur : solver.Assert(result.Subgoals[0].Formulas) 5. Tactiques a tester : "simplify", "bit-blast", "ctx-solver-simplify", "solve-eqs"

Vérification : "bit-blast" est généralement efficace pour les BitVectors.

// Exercice 3 : Comparaison des tactiques Z3
using Microsoft.Z3;
using System.Diagnostics;

var tacticPuzzle = SudokuHelper.GetSudokus(SudokuDifficulty.Medium).First();
var tacticCtx = Z3BitVectorSolverBase.ctx;
var genericConstr = Z3BitVectorSolverBase.GenericContraints;
var puzzleConstrHelper = new Z3BitVectorSolverSimple();
var puzzleConstr = puzzleConstrHelper.GetPuzzleConstraints(tacticPuzzle);

string[] tacticNames = { "simplify", "ctx-solver-simplify", "bit-blast", "solve-eqs" };

Console.WriteLine("Comparaison des tactiques Z3 :");
Console.WriteLine(new string('-', 40));

// TODO : Pour chaque tactique, créer et appliquer, mesurer le temps de résolution
// foreach (var tacticName in tacticNames)
// {
//     var tactic = tacticCtx.MkTactic(tacticName);
//     var goal = tacticCtx.MkGoal();
//     goal.Assert(tacticCtx.MkAnd(genericConstr, puzzleConstr));
//     var sw = Stopwatch.StartNew();
//     var result = tactic.Apply(goal);
//     var solver = tacticCtx.MkSolver();
//     if (result.NumSubgoals > 0)
//         solver.Assert(result.Subgoals[0].Formulas);
//     var status = solver.Check();
//     sw.Stop();
//     Console.WriteLine($"{tacticName,-25} : {sw.ElapsedMilliseconds,6} ms - {status}");
// }

Console.WriteLine("TODO : Implementez la comparaison des tactiques Z3");
Comparaison des tactiques Z3 :
----------------------------------------
TODO : Implementez la comparaison des tactiques Z3

Exercice : Vérification de propriétés avec Z3

Enonce

Utilisez Z3 pour vérifier des propriétés logiques sur les grilles de Sudoku. Implémentez les fonctions suivantes avec l’API Z3 en C# :

  1. HasUniqueSolution(SudokuGrid puzzle) : Vérifie si une grille a exactement une solution
    • Trouver la première solution S1
    • Ajouter la contrainte “la solution n’est pas S1”
    • Si aucune deuxième solution -> unicité vérifiée
  2. IsMinimal(SudokuGrid puzzle) : Vérifie si le puzzle est minimal (supprimer une valeur initiale crée une ambiguïté)
    • Pour chaque cellule fixe (r, c) avec valeur v :
      • Créer une grille sans cette cellule
      • Vérifier que HasUniqueSolution retourne false (plus d’une solution)
  3. Testez avec le puzzle facile : vérifiez unicité et minimalité

Indice :

Pour HasUniqueSolution, après avoir trouvé S1 = {cells[i][j] = v[i][j]}, ajoutez la contrainte Or(cell[i][j] != v[i][j]) pour toutes les cellules. Cette contrainte dit “au moins une cellule diffère de S1”.

// Exercice : Vérification de propriétés avec Z3

public class Z3SudokuPropertyChecker
{
    private static Context ctx = Z3IntSolverSimple.ctx;

    /// <summary>
    /// Vérifie si un puzzle a exactement une solution.
    /// Strategie : trouver S1, puis chercher S2 != S1. Si impossible -> unique.
    /// </summary>
    public bool HasUniqueSolution(SudokuGrid puzzle)
    {
        // TODO : Implémenter la vérification d'unicité
        // 1. Construire les contraintes generiques + contraintes du puzzle
        // 2. Trouver la première solution S1
        // 3. Ajouter la contrainte "au moins une cellule differe de S1"
        // 4. Vérifier si une deuxième solution existe
        return false;
    }

    /// <summary>
    /// Vérifie si le puzzle est minimal :
    /// supprimer n'importe quelle valeur initiale crée une ambiguïté.
    /// </summary>
    public bool IsMinimal(SudokuGrid puzzle)
    {
        // TODO : Implémenter la vérification de minimalité
        // Pour chaque cellule fixee (i, j) :
        //   - Créer une copie du puzzle sans la valeur en (i, j)
        //   - Vérifier que HasUniqueSolution retourne false
        // Si toutes les cellules satisfont cette condition -> minimal
        return false;
    }
}

// Test : vérifier les propriétés sur le puzzle facile
var checker = new Z3SudokuPropertyChecker();
var easyPuzzle = SudokuHelper.GetSudokus(SudokuDifficulty.Hard).First();
Console.WriteLine("Test de verification de proprietes Z3");
Console.WriteLine("Puzzle selectionne :");
Console.WriteLine(easyPuzzle);
// bool unique = checker.HasUniqueSolution(easyPuzzle);
// bool minimal = checker.IsMinimal(easyPuzzle);
// Console.WriteLine($"Solution unique : {unique}");
// Console.WriteLine($"Puzzle minimal : {minimal}");
Test de verification de proprietes Z3
Puzzle selectionne :
-------------------------------
| 4       |         | 8     5 | 
|    3    |         |         | 
|         | 7       |         | 
-------------------------------
|    2    |         |    6    | 
|         |    8    | 4       | 
|         |    1    |         | 
-------------------------------
|         | 6     3 |    7    | 
| 5       | 2       |         | 
| 1     4 |         |         | 
-------------------------------

A retenir

Z3 offre quatre formulations de résolution Sudoku, de la plus simple à la plus optimisée :

Formulation Variables Avantage
IntExpr simple 81 IntVar Modélisation directe, facile à comprendre
BitVec 4 bits 81 BitVec Espace reduit (4 bits vs 32 bits)
Substitution API 81 BitVec Réutilisation du modèle générique
Tactiques 81 BitVec Pre-traitement (simplify, bit-blast)

Lecons : 1. L’API Substitution permet de séparer le modèle générique (contraintes Sudoku) des valeurs spécifiques au puzzle. 2. Les tactiques (simplify, bit-blast, ctx-solver-simplify) pré-traitent les formules pour accélérer la résolution. 3. L’exclusion de modèle (model blocking) vérifie l’unicité de la solution en ajoutant des contraintes d’exclusion. 4. Z3 reste l’outil de référence pour la vérification formelle de propriétés (unicité, minimalité).

Navigation : << Sudoku-11 Choco C# | Index | Sudoku-13 Symbolic Automata C# >>

Voir aussi : - CSP-3-Avance - Contraintes globales avancees - SymbolicAI - Série sur l’IA symbolique et Z3

Retour au sommet