Navigation : Index | << Sudoku-13 C# | Sudoku-15 C# >>

Sudoku-14 : Automates avec BDD/MDD - Approche Pure

Dans ce notebook, nous implémentons une vraie approche par automates symboliques utilisant des Binary Decision Diagrams (BDD) et Multi-valued Decision Diagrams (MDD). Contrairement à Sudoku-12 qui compilait vers Z3, cette approche construit explicitement des automates avec des états et des transitions.

Qu’est-ce qu’un BDD?

Un BDD (Binary Decision Diagram) est une structure de données compacte pour représenter des fonctions booléennes. C’est le graphe de décision d’une fonction booléenne, partageant les sous-graphes isomorphes.

Concept	Description
Nœud	Variable booléenne (x, y, z, …)
Arc	0 (false) ou 1 (true)
Feuille	0 ou 1 (résultat)
BDD réduit	Sans redondance, sans nœuds inutiles

Un MDD généralise le BDD aux domaines finis (comme {1,2,…,9} pour Sudoku).

Objectifs d’apprentissage

À la fin de ce notebook, vous saurez :

Comprendre la structure des BDD et leur réduction
Implémenter un BDD simple en C#
Construire un MDD pour les domaines Sudoku
Composer des automates avec produit d’automates explicite
Apprécier la différence avec l’approche Z3 (Sudoku-12)

Prérequis

Sudoku-0-Environment - Classes de base Sudoku
Sudoku-13-SymbolicAutomata - Théorie des automates (recommandée)
Connaissance de base des graphes et arbres

Durée estimée : 25 min

Références

Andersen, H. R. - “An Introduction to Binary Decision Diagrams” (1997)
Bryant, R. E. - “Graph-Based Algorithms for Boolean Function Manipulation” (1986)
Somenzi, F. - “Binary Decision Diagrams” (1999)

Note sur l’approche :

⚠️ Important : Ce notebook implémente une approche “pure” automata avec BDD/MDD, sans utiliser Z3. Cette approche est moins performante que Z3 mais illustre la théorie des automates symboliques de manière plus authentique.

1. Introduction - BDD vs Z3 (10 min)

1.1 Comparaison des Approches

Aspect	BDD/MDD (ce notebook)	Z3 SMT (Sudoku-12)
Structure	Graphe de décision explicite	Formules logiques
Opérations	Union, Intersection, Réduction	SAT solving
Mémoïsation	Naturelle (partage de sous-graphes)	Via Z3
Performance	(mesure, voir cellule precedente)	(mesure, voir cellule precedente)
Authenticité	⭐⭐⭐ Vrais automates	⭐⭐ Compilation

1.2 Pourquoi BDD?

Avantages : - Représentation canonique (forme unique pour une fonction) - Opérations booléennes efficaces (AND, OR, NOT) - Mémoïsation automatique

Inconvénients : - Taille peut exploser pour certaines fonctions - Moins performant que Z3 pour les contraintes arithmétiques

1.3 MDD pour Sudoku

Pour Sudoku, nous utilisons des MDD (Multi-valued Decision Diagrams) car chaque cellule a un domaine de {1, 2, …, 9} au lieu de {0, 1}.

MDD pour une cellule Sudoku:

        racine
       / | ... \
     1   2  ...  9
     |   |      |
    feuille (valeur choisie)

Note (mandat #9377/#9434) : les durées wall-clock (< 1 ms, ~ 20 ms) de cette table comparative sont machine-dépendantes par construction (compile .NET + JIT + GC, charge CPU du runner) et drainées. Le rapport d’ordres de grandeur (BDD ≈≪ Z3 sur ce puzzle) est reproductible d’une exécution à l’autre et conservé. Les mesures exactes restent visibles dans les cellules de mesure amont (§6 du présent notebook pour la mesure BDD/MDD ; cellule de banc d’essai [24] du notebook Sudoku-12-Z3-CSharp pour la mesure Z3). La pédagogie de cette cellule tient sur la discrimination théorique (vrais automates vs compilation SMT), pas sur les ratios quantitatifs qui rebougent à chaque machine.

2. Implémentation d’un BDD Simple (15 min)

2.1 Structure du BDD

Commençons par implémenter un BDD simple pour des fonctions booléennes.

using System;
using System.Collections.Generic;
using System.Linq;

/// <summary>
/// Nœud d'un BDD (Binary Decision Diagram).
/// Un nœud représente une variable booléenne avec deux enfants :
/// - childFalse : résultat quand la variable est false
/// - childTrue : résultat quand la variable est true
/// </summary>
public class BDDNode
{
    public string Variable { get; }
    public BDDNode ChildFalse { get; }
    public BDDNode ChildTrue { get; }
    public bool IsTerminal { get; }
    public bool Value { get; }

    // Nœud terminal (feuille)
    private BDDNode(bool value)
    {
        IsTerminal = true;
        Value = value;
        Variable = null;
        ChildFalse = null;
        ChildTrue = null;
    }

    // Nœud interne
    private BDDNode(string variable, BDDNode childFalse, BDDNode childTrue)
    {
        IsTerminal = false;
        Value = false;
        Variable = variable;
        ChildFalse = childFalse;
        ChildTrue = childTrue;
    }

    // Singleton pour les terminaux
    private static readonly BDDNode _true = new BDDNode(true);
    private static readonly BDDNode _false = new BDDNode(false);

    public static BDDNode True => _true;
    public static BDDNode False => _false;

    public static BDDNode Create(string variable, BDDNode childFalse, BDDNode childTrue)
    {
        // Réduction : si les deux enfants sont identiques, retourner l'enfant
        if (childFalse == childTrue)
            return childFalse;
        
        // Réduction : si variable est inutile, retourner l'enfant approprié
        // (c'est une simplification, la vraie réduction est plus complexe)
        
        return new BDDNode(variable, childFalse, childTrue);
    }

    /// <summary>
    /// Évalue le BDD pour une assignation de variables.
    /// </summary>
    public bool Evaluate(Dictionary<string, bool> assignment)
    {
        if (IsTerminal)
            return Value;
        
        bool varValue = assignment.GetValueOrDefault(Variable, false);
        BDDNode nextChild = varValue ? ChildTrue : ChildFalse;
        return nextChild.Evaluate(assignment);
    }

    /// <summary>
    /// Compte le nombre de nœuds dans le BDD.
    /// </summary>
    public int CountNodes()
    {
        if (IsTerminal)
            return 1;
        
        return 1 + ChildFalse.CountNodes() + ChildTrue.CountNodes();
    }

    /// <summary>
    /// Retourne une représentation textuelle du BDD.
    /// </summary>
    public string ToString(string indent = "")
    {
        if (IsTerminal)
            return $"{indent}({Value})";
        
        var sb = new System.Text.StringBuilder();
        sb.AppendLine($"{indent}{Variable}?");
        sb.AppendLine($"{indent}  |-> {ChildTrue.ToString(indent + "  |").Trim()}");
        sb.Append($"{indent}  |-> {ChildFalse.ToString(indent + "  |").Trim()}");
        return sb.ToString();
    }

    public override string ToString() => ToString("");
}

Console.WriteLine("Classe BDDNode definie avec succes.");
Console.WriteLine("Operations disponibles :");
Console.WriteLine("  - True/False : Terminaux (feuilles)");
Console.WriteLine("  - Create(var, low, high) : Cree un noeud de decision");
Console.WriteLine("  - Evaluate(assign) : Evalue le BDD");
Console.WriteLine("  - CountNodes() : Compte les noeuds");

Classe BDDNode definie avec succes.
Operations disponibles :
  - True/False : Terminaux (feuilles)
  - Create(var, low, high) : Cree un noeud de decision
  - Evaluate(assign) : Evalue le BDD
  - CountNodes() : Compte les noeuds

2.2 Exemples de BDD

Créons quelques BDD simples pour comprendre la structure.

Exercice : Construire un BDD pour la contrainte “exactement un parmi N”

Objectif : Construisez un BDD qui encode la contrainte : parmi N variables booléennes, exactement une doit être vraie.

Indice : Utilisez la négation et la conjonction pour exprimer la contrainte.

// EXERCICE : Construire un BDD pour la contrainte "exactement un parmi N"
public BDDNode ExactlyOneOfN(BDDNode[] variables)
{
    // TODO: Construisez un BDD qui est vrai si exactement une des N variables est vraie
    return null; // TODO etudiant
}
Console.WriteLine("Exercice a completer");

Exercice a completer

// Exemple 1 : BDD pour la fonction constante TRUE
var bddTrue = BDDNode.True;
Console.WriteLine("=== Exemple 1 : Constante TRUE ===");
Console.WriteLine($"Noeuds : {bddTrue.CountNodes()}");
Console.WriteLine($"Valeur : {bddTrue.Evaluate(new Dictionary<string, bool>())}");
Console.WriteLine();

// Exemple 2 : BDD pour une variable simple x
var bddX = BDDNode.Create("x", BDDNode.False, BDDNode.True);
Console.WriteLine("=== Exemple 2 : Variable x ===");
Console.WriteLine(bddX.ToString());
Console.WriteLine($"Noeuds : {bddX.CountNodes()}");
Console.WriteLine($"Eval(x=true) : {bddX.Evaluate(new Dictionary<string, bool> {{"x", true}})}");
Console.WriteLine($"Eval(x=false) : {bddX.Evaluate(new Dictionary<string, bool> {{"x", false}})}");
Console.WriteLine();

// Exemple 3 : BDD pour x AND y
// x AND y = si x est false, alors false; si x est true, alors résultat = y
var bddY = BDDNode.Create("y", BDDNode.False, BDDNode.True);
var bddXAndY = BDDNode.Create("x", BDDNode.False, bddY);
Console.WriteLine("=== Exemple 3 : x AND y ===");
Console.WriteLine(bddXAndY.ToString());
Console.WriteLine($"Noeuds : {bddXAndY.CountNodes()}");
Console.WriteLine($"Eval(x=true, y=true) : {bddXAndY.Evaluate(new Dictionary<string, bool> {{"x", true}, {"y", true}})}");
Console.WriteLine($"Eval(x=true, y=false) : {bddXAndY.Evaluate(new Dictionary<string, bool> {{"x", true}, {"y", false}})}");
Console.WriteLine($"Eval(x=false, y=true) : {bddXAndY.Evaluate(new Dictionary<string, bool> {{"x", false}, {"y", true}})}");

=== Exemple 1 : Constante TRUE ===
Noeuds : 1
Valeur : True

=== Exemple 2 : Variable x ===
x?
  |-> |(True)
  |-> |(False)
Noeuds : 3
Eval(x=true) : True
Eval(x=false) : False

=== Exemple 3 : x AND y ===
x?
  |-> |y?
  |  |-> |  |(True)
  |  |-> |  |(False)
  |-> |(False)
Noeuds : 5
Eval(x=true, y=true) : True
Eval(x=true, y=false) : False
Eval(x=false, y=true) : False

Interprétation : Exemples de BDD

Sortie obtenue :

Constante TRUE : Un seul nœud terminal avec valeur true
Variable x : 3 nœuds (racine x + 2 terminaux)
x AND y : 5 nœuds (structure d’arbre binaire)

Table de vérité x AND y :

x	y	x AND y
F	F	F
F	T	F
T	F	F
T	T	T

Point important : Le BDD pour x AND y a 5 nœuds. Si nous appliquions la réduction complète (partage de sous-graphes identiques), nous aurions moins de nœuds car les terminaux False sont partagés.

3. Opérations sur les BDD (15 min)

3.1 Opération AND (Apply)

L’opération de base sur les BDD est Apply qui combine deux BDD avec une fonction booléenne (AND, OR, XOR, etc.).

using System;
using System.Collections.Generic;

/// <summary>
/// Opérations sur les BDD : Apply (op binaire), And/Or/Not.
/// Version pédagogique: réduction locale via BDDNode.Create.
/// </summary>
public static class BDDOperations
{
    // Cache (computed table) : (f,g,opName) -> result
    private static readonly Dictionary<(BDDNode f, BDDNode g, string op), BDDNode> _cache
        = new();

    public static BDDNode Apply(BDDNode f, BDDNode g, Func<bool, bool, bool> op, string opName)
    {
        // Terminal / terminal
        if (f.IsTerminal && g.IsTerminal)
            return op(f.Value, g.Value) ? BDDNode.True : BDDNode.False;

        // Memoization
        var key = (f, g, opName);
        if (_cache.TryGetValue(key, out var cached))
            return cached;

        // Choix de la variable "top" (ordre alphabétique simple)
        // Les terminaux sont traités comme "pas de variable", donc l'autre gagne.
        string topVar;
        if (f.IsTerminal) topVar = g.Variable;
        else if (g.IsTerminal) topVar = f.Variable;
        else topVar = string.CompareOrdinal(f.Variable, g.Variable) <= 0 ? f.Variable : g.Variable;

        // Cofacteurs (Shannon expansion)
        BDDNode fLow, fHigh, gLow, gHigh;

        if (!f.IsTerminal && f.Variable == topVar)
        {
            fLow = f.ChildFalse; fHigh = f.ChildTrue;
        }
        else
        {
            fLow = fHigh = f; // f ne dépend pas de topVar
        }

        if (!g.IsTerminal && g.Variable == topVar)
        {
            gLow = g.ChildFalse; gHigh = g.ChildTrue;
        }
        else
        {
            gLow = gHigh = g; // g ne dépend pas de topVar
        }

        var low = Apply(fLow, gLow, op, opName);
        var high = Apply(fHigh, gHigh, op, opName);

        var result = BDDNode.Create(topVar, low, high);
        _cache[key] = result;
        return result;
    }

    public static BDDNode And(BDDNode f, BDDNode g) => Apply(f, g, (a, b) => a && b, "AND");
    public static BDDNode Or(BDDNode f, BDDNode g)  => Apply(f, g, (a, b) => a || b, "OR");

    public static BDDNode Not(BDDNode f)
    {
        if (f.IsTerminal) return f.Value ? BDDNode.False : BDDNode.True;
        return BDDNode.Create(f.Variable, Not(f.ChildFalse), Not(f.ChildTrue));
    }
}

Console.WriteLine("BDDOperations OK (Apply/And/Or/Not).");

BDDOperations OK (Apply/And/Or/Not).

3.2 Test des Opérations

Testons les opérations BDD avec des exemples simples.

// Test 1 : x AND NOT x = FALSE
var bddX = BDDNode.Create("x", BDDNode.False, BDDNode.True);
var bddNotX = BDDOperations.Not(bddX);
var bddXAndNotX = BDDOperations.And(bddX, bddNotX);

Console.WriteLine("=== Test 1 : x AND NOT x ===");
Console.WriteLine($"Resultat : {bddXAndNotX.Evaluate(new Dictionary<string, bool>())}");
Console.WriteLine($"Attendu : False");
Console.WriteLine($"Noeuds : {bddXAndNotX.CountNodes()}");
Console.WriteLine();

// Test 2 : x OR NOT x = TRUE
var bddXOrNotX = BDDOperations.Or(bddX, bddNotX);
Console.WriteLine("=== Test 2 : x OR NOT x ===");
Console.WriteLine($"Resultat : {bddXOrNotX.Evaluate(new Dictionary<string, bool>())}");
Console.WriteLine($"Attendu : True");
Console.WriteLine($"Noeuds : {bddXOrNotX.CountNodes()}");
Console.WriteLine();

// Test 3 : (x AND y) OR (x AND z) = x AND (y OR z)
var bddY = BDDNode.Create("y", BDDNode.False, BDDNode.True);
var bddZ = BDDNode.Create("z", BDDNode.False, BDDNode.True);
var bddXAndY = BDDOperations.And(bddX, bddY);
var bddXAndZ = BDDOperations.And(bddX, bddZ);
var bddLeft = BDDOperations.Or(bddXAndY, bddXAndZ);

var bddYOrZ = BDDOperations.Or(bddY, bddZ);
var bddRight = BDDOperations.And(bddX, bddYOrZ);

Console.WriteLine("=== Test 3 : Distributivite ===");
Console.WriteLine($"Noeuds (gauche) : {bddLeft.CountNodes()}");
Console.WriteLine($"Noeuds (droite) : {bddRight.CountNodes()}");
Console.WriteLine($"Equivalent (x=T,y=T,z=F) : {bddLeft.Evaluate(new Dictionary<string, bool> {{"x", true}, {"y", true}, {"z", false}})} == {bddRight.Evaluate(new Dictionary<string, bool> {{"x", true}, {"y", true}, {"z", false}})}");

=== Test 1 : x AND NOT x ===
Resultat : False
Attendu : False
Noeuds : 1

=== Test 2 : x OR NOT x ===
Resultat : True
Attendu : True
Noeuds : 1

=== Test 3 : Distributivite ===
Noeuds (gauche) : 7
Noeuds (droite) : 7
Equivalent (x=T,y=T,z=F) : True == True

Interprétation : Test des Opérations

Sortie obtenue :

Test 1 (x AND NOT x) : résultat False, 1 seul nœud
Test 2 (x OR NOT x) : résultat True, 1 seul nœud
Test 3 (distributivité) : 7 nœuds pour chaque membre, équivalence vérifiée sur (x=T, y=T, z=F)

Les deux premiers tests illustrent la normalisation : une contradiction ou une tautologie, quelle que soit la taille de l’expression qui l’écrit, se réduit au terminal correspondant — ici un unique nœud, contre 3 pour la variable x seule. Le BDD ne stocke pas la syntaxe de la formule, mais la fonction qu’elle dénote ; deux expressions équivalentes convergent donc vers le même diagramme.

Le test 3 le montre sur un cas non trivial : x AND (y OR z) et (x AND y) OR (x AND z) sont deux écritures distinctes de la même fonction. Après construction, les deux BDD comptent 7 nœuds chacun et s’évaluent identiquement. La distributivité n’a pas été invoquée comme règle de réécriture : elle est devenue structurellement visible — mêmes diagrammes, même fonction. C’est cette canonicité qui permet de répondre « ces deux circuits logiques sont-ils équivalents ? » par une simple comparaison de graphes, sans énumérer la table de vérité.

4. MDD pour Sudoku (20 min)

4.1 De BDD à MDD

Les BDD sont parfaits pour des variables booléennes, mais Sudoku utilise des variables à valeurs dans {1, …, 9}. Nous avons besoin de MDD (Multi-valued Decision Diagrams).

BDD (binaire)          MDD (multi-value)
    x?                     x?
   / \                  / | \ \
  0   1                1  2 ... 9

using System;
using System.Collections.Generic;
using System.Linq;

/// <summary>
/// Nœud d'un MDD (Multi-valued Decision Diagram) pour Sudoku.
/// </summary>
public class MDDNode
{
    public string CellName { get; }
    public Dictionary<int, MDDNode> Children { get; }
    public bool IsTerminal { get; }
    public bool IsValid { get; }

    private MDDNode(bool isValid)
    {
        IsTerminal = true;
        IsValid = isValid;
        CellName = null;
        Children = null;
    }

    private MDDNode(string cellName, Dictionary<int, MDDNode> children)
    {
        IsTerminal = false;
        IsValid = false;
        CellName = cellName;
        Children = children;
    }

    private static readonly MDDNode _valid = new MDDNode(true);
    private static readonly MDDNode _invalid = new MDDNode(false);

    public static MDDNode Valid => _valid;
    public static MDDNode Invalid => _invalid;

    public static MDDNode Create(string cellName, Dictionary<int, MDDNode> children)
    {
        if (children.Count == 0) return Invalid;

        // Réduction simple
        var first = children.Values.First();
        if (children.Values.All(c => ReferenceEquals(c, first)))
            return first;

        if (children.Values.All(c => ReferenceEquals(c, Invalid)))
            return Invalid;

        return new MDDNode(cellName, children);
    }

    public bool Evaluate(Dictionary<string, int> assignment)
    {
        if (IsTerminal) return IsValid;
        if (!assignment.TryGetValue(CellName, out var v)) return false;
        if (!Children.TryGetValue(v, out var child)) return false;
        return child.Evaluate(assignment);
    }

    public int CountNodes()
    {
        if (IsTerminal) return 1;
        return 1 + Children.Values.Sum(c => c.CountNodes());
    }

    public string Pretty(string indent = "")
    {
        if (IsTerminal) return $"{indent}({(IsValid ? "VALID" : "INVALID")})";

        var lines = new List<string> { $"{indent}{CellName}?" };
        foreach (var (k, v) in Children.OrderBy(kvp => kvp.Key))
            lines.Add($"{indent}  {k} -> {v.Pretty(indent + "  |  ").Trim()}");
        return string.Join("\n", lines);
    }

    public override string ToString() => Pretty();
}

Console.WriteLine("MDDNode OK (Pretty/ToString/Evaluate).");

MDDNode OK (Pretty/ToString/Evaluate).

4.2 MDD pour une Contrainte de Ligne

Créons un MDD pour représenter la contrainte “les 9 valeurs d’une ligne sont distinctes”.

Note : Cette représentation est naïve et conduit à une explosion d’états. Nous verrons comment optimiser.

using System;
using System.Collections.Generic;

/// <summary>
/// Constructeur de MDD pour la contrainte "ligne = 9 valeurs distinctes".
/// Mémoïsation via (col, usedMask) pour partager les sous-graphes.
/// </summary>
public class RowMDDBuilder
{
    private readonly int _rowIndex;
    private readonly Dictionary<(int col, int mask), MDDNode> _memo = new();

    public RowMDDBuilder(int rowIndex) => _rowIndex = rowIndex;

    public MDDNode Build() => BuildRecursive(0, 0);

    // mask: bit v-1 à 1 si la valeur v est déjà utilisée
    private MDDNode BuildRecursive(int col, int usedMask)
    {
        if (col >= 9) return MDDNode.Valid;

        var key = (col, usedMask);
        if (_memo.TryGetValue(key, out var cached))
            return cached;

        string cellName = $"r{_rowIndex}_c{col}";
        var children = new Dictionary<int, MDDNode>();

        for (int v = 1; v <= 9; v++)
        {
            int bit = 1 << (v - 1);
            if ((usedMask & bit) != 0)
            {
                children[v] = MDDNode.Invalid;
            }
            else
            {
                children[v] = BuildRecursive(col + 1, usedMask | bit);
            }
        }

        var node = MDDNode.Create(cellName, children);
        _memo[key] = node;
        return node;
    }
}

Console.WriteLine("RowMDDBuilder OK (memoization bitmask).");

RowMDDBuilder OK (memoization bitmask).

Interprétation : Clé d’état du constructeur

Sortie obtenue : RowMDDBuilder OK (memoization bitmask) — la classe est enregistrée, prête pour la construction de la section suivante.

Le cœur du constructeur est sa clé de mémoïsation : l’état (col, usedMask), où usedMask est un bitmask sur 9 bits — le bit v−1 vaut 1 si la valeur v est déjà posée dans la ligne. Conceptuellement, deux branches qui arrivent à la même colonne avec le même ensemble de valeurs posées décrivent le même état du problème, quel que soit l’ordre dans lequel ces valeurs ont été choisies : elles peuvent donc légitimement partager le même sous-graphe au lieu de le reconstruire. C’est cette notion d’état canonique (colonne × ensemble, pas séquence) qui fonde tous les partages de sous-graphes en diagrammes de décision.

La mesure de la section suivante montrera ce que ce partage vaut effectivement dans cette implémentation — et pourquoi le solveur de fin de notebook s’en tient à une version simplifiée plutôt que de construire les 27 MDD complets.

4.3 Test du MDD de Ligne

Attention : Le MDD complet pour une ligne à 9! = 362880 chemins valides. La construction va prendre du temps!

Exercice : Construire un MDD pour la contrainte “tous différents”

Objectif : Construisez un MDD (Multi-valued Decision Diagram) qui encode la contrainte “tous différents” pour une ligne de 9 cellules avec valeurs 1-9.

Indice : Chaque niveau du MDD représente une cellule, et chaque arc représente une valeur possible non encore utilisée.

// EXERCICE : Construire un MDD pour la contrainte "tous différents"
public MDDNode BuildAllDifferentMDD(int numCells, int maxValue)
{
    // TODO: Construisez un MDD qui accepte uniquement les assignments
    // ou toutes les valeurs sont différentes
    return null; // TODO etudiant
}
Console.WriteLine("Exercice a completer");

Exercice a completer

// Construction du MDD pour la ligne 0
// Note: Cela peut prendre quelques secondes car 9! chemins

Console.WriteLine("Construction du MDD pour une ligne Sudoku...");
Console.WriteLine("Attention: 9! = 362880 permutations valides");

var builder = new RowMDDBuilder(0);
var rowMDD = builder.Build();

Console.WriteLine($"MDD construit!");
Console.WriteLine($"Nombre de noeuds : {rowMDD.CountNodes()}");
Console.WriteLine();

// Test 1 : Ligne valide (permutation)
var validAssignment = new Dictionary<string, int>
{
    {"r0_c0", 1}, {"r0_c1", 2}, {"r0_c2", 3},
    {"r0_c3", 4}, {"r0_c4", 5}, {"r0_c5", 6},
    {"r0_c6", 7}, {"r0_c7", 8}, {"r0_c8", 9}
};

Console.WriteLine("=== Test 1 : Ligne valide ===");
Console.WriteLine($"Resultat : {rowMDD.Evaluate(validAssignment)}");
Console.WriteLine($"Attendu : True");
Console.WriteLine();

// Test 2 : Ligne invalide (doublon)
var invalidAssignment = new Dictionary<string, int>
{
    {"r0_c0", 1}, {"r0_c1", 1}, {"r0_c2", 3},
    {"r0_c3", 4}, {"r0_c4", 5}, {"r0_c5", 6},
    {"r0_c6", 7}, {"r0_c7", 8}, {"r0_c8", 9}
};

Console.WriteLine("=== Test 2 : Ligne invalide (doublon de 1) ===");
Console.WriteLine($"Resultat : {rowMDD.Evaluate(invalidAssignment)}");
Console.WriteLine($"Attendu : False");

Construction du MDD pour une ligne Sudoku...
Attention: 9! = 362880 permutations valides
MDD construit!
Nombre de noeuds : 5611771

=== Test 1 : Ligne valide ===
Resultat : True
Attendu : True

=== Test 2 : Ligne invalide (doublon de 1) ===
Resultat : False
Attendu : False

Interprétation : MDD de Ligne

Sortie obtenue :

Le MDD construit comporte 5 611 771 nœuds, soit environ 15 fois 9! (362 880 permutations valides) : à cette échelle, l’explosion combinatoire des branches l’emporte
Seul le partage des terminaux est appliqué ; la réduction complète des sous-graphes identiques reste un exercice (voir plus bas), d’où la taille élevée
L’évaluation est correcte pour les lignes valides et invalides

Comparaison :

Approche	Structure	Taille
Automate naïve (explicite)	9! états	~360K
MDD (ce notebook)	Diagramme multi-value	~5,6 millions de nœuds

Point important : Même avec réduction, le MDD pour une seule ligne est déjà assez grand. Pour un Sudoku complet (81 cellules), l’explosion serait monumentale.

5. Produit d’Automates Explicite (15 min)

5.1 Produit de MDD

Pour combiner plusieurs contraintes (ligne + colonne + bloc), nous devons faire le produit d’automates. Contrairement à Sudoku-12 qui compilait vers Z3, nous allons construire explicitement ce produit.

using System;
using System.Collections.Generic;
using System.Linq;

/// <summary>
/// Produit (intersection) de deux MDD.
/// </summary>
public static class MDDOperations
{
    public static MDDNode Product(MDDNode f, MDDNode g)
        => ProductRecursive(f, g, new Dictionary<(MDDNode, MDDNode), MDDNode>());

    private static MDDNode ProductRecursive(
        MDDNode f,
        MDDNode g,
        Dictionary<(MDDNode, MDDNode), MDDNode> cache)
    {
        // Terminaux
        if (f.IsTerminal && g.IsTerminal)
            return (f.IsValid && g.IsValid) ? MDDNode.Valid : MDDNode.Invalid;

        if (f.IsTerminal) return f.IsValid ? g : MDDNode.Invalid;
        if (g.IsTerminal) return g.IsValid ? f : MDDNode.Invalid;

        var key = (f, g);
        if (cache.TryGetValue(key, out var cached))
            return cached;

        MDDNode result;

        if (f.CellName == g.CellName)
        {
            // Même variable : intersection des arcs
            var values = f.Children.Keys.Intersect(g.Children.Keys).ToList();
            var children = new Dictionary<int, MDDNode>();

            foreach (var v in values)
                children[v] = ProductRecursive(f.Children[v], g.Children[v], cache);

            result = MDDNode.Create(f.CellName, children);
        }
        else
        {
            // Ordre lexicographique des variables (pédagogique)
            if (string.CompareOrdinal(f.CellName, g.CellName) < 0)
            {
                var children = new Dictionary<int, MDDNode>();
                foreach (var (v, child) in f.Children)
                    children[v] = ProductRecursive(child, g, cache);

                result = MDDNode.Create(f.CellName, children);
            }
            else
            {
                var children = new Dictionary<int, MDDNode>();
                foreach (var (v, child) in g.Children)
                    children[v] = ProductRecursive(f, child, cache);

                result = MDDNode.Create(g.CellName, children);
            }
        }

        cache[key] = result;
        return result;
    }
}

Console.WriteLine("MDDOperations OK (Product).");

MDDOperations OK (Product).

5.2 Test du Produit

Testons le produit avec un petit exemple : une grille 2x2 au lieu de 9x9.

// Pour simplifier, travaillons avec une grille 2x2 (valeurs 1-2)
// Cela nous permet de voir la structure du produit

/// <summary>
/// Constructeur d'MDD pour une ligne de taille 2.
/// </summary>
public class SmallRowMDDBuilder
{
    private string _rowPrefix;
    private int _size;
    private int _maxValue;
    
    public SmallRowMDDBuilder(string rowPrefix, int size, int maxValue)
    {
        _rowPrefix = rowPrefix;
        _size = size;
        _maxValue = maxValue;
    }
    
    public MDDNode Build()
    {
        return BuildRecursive(0, new HashSet<int>());
    }
    
    private MDDNode BuildRecursive(int col, HashSet<int> usedValues)
    {
        if (col >= _size)
            return MDDNode.Valid;
        
        string cellName = $"{_rowPrefix}_c{col}";
        var children = new Dictionary<int, MDDNode>();
        
        for (int v = 1; v <= _maxValue; v++)
        {
            if (usedValues.Contains(v))
                children[v] = MDDNode.Invalid;
            else
            {
                var newUsed = new HashSet<int>(usedValues) { v };
                children[v] = BuildRecursive(col + 1, newUsed);
            }
        }
        
        return MDDNode.Create(cellName, children);
    }
}

Console.WriteLine("=== Test du Produit MDD ===");
Console.WriteLine("Grille 2x2 (valeurs 1-2)");
Console.WriteLine();

// MDD pour la ligne 0 : r0_c0 et r0_c1 doivent être distincts
var row0Builder = new SmallRowMDDBuilder("r0", 2, 2);
var row0MDD = row0Builder.Build();

Console.WriteLine("MDD Ligne 0 (2 cellules, valeurs 1-2) :");
Console.WriteLine($"Noeuds : {row0MDD.CountNodes()}");
Console.WriteLine();

// MDD pour la colonne 0 : r0_c0 et r1_c0 doivent être distincts
var col0Builder = new SmallRowMDDBuilder("c0", 2, 2);  // Reutilise le meme constructeur
// Note: Pour la vraie colonne, il faudrait un constructeur différent
// Ici on simplifie en traitant comme une "ligne" c0_0 et c0_1

// Pour le test, créons une contrainte simple : r0_c0 != 1
var notOneChildren = new Dictionary<int, MDDNode>
{
    {1, MDDNode.Invalid},
    {2, MDDNode.Valid}
};
var notOneMDD = MDDNode.Create("r0_c0", notOneChildren);

Console.WriteLine("MDD Contrainte (r0_c0 != 1) :");
Console.WriteLine(notOneMDD.ToString());
Console.WriteLine();

// Produit : ligne 0 ET (r0_c0 != 1)
var productMDD = MDDOperations.Product(row0MDD, notOneMDD);

Console.WriteLine("MDD Produit (ligne 0 INTERSECT r0_c0 != 1) :");
Console.WriteLine($"Noeuds : {productMDD.CountNodes()}");

// Test : r0_c0=1, r0_c1=2 devrait être rejecte par le produit
var testAssign1 = new Dictionary<string, int> {{"r0_c0", 1}, {"r0_c1", 2}};
Console.WriteLine($"Test (r0_c0=1, r0_c1=2) : {productMDD.Evaluate(testAssign1)} (attendu: False)");

// Test : r0_c0=2, r0_c1=1 devrait être accepté
var testAssign2 = new Dictionary<string, int> {{"r0_c0", 2}, {"r0_c1", 1}};
Console.WriteLine($"Test (r0_c0=2, r0_c1=1) : {productMDD.Evaluate(testAssign2)} (attendu: True)");

=== Test du Produit MDD ===
Grille 2x2 (valeurs 1-2)

MDD Ligne 0 (2 cellules, valeurs 1-2) :
Noeuds : 7

MDD Contrainte (r0_c0 != 1) :
r0_c0?
  1 -> |  (INVALID)
  2 -> |  (VALID)

MDD Produit (ligne 0 INTERSECT r0_c0 != 1) :
Noeuds : 5
Test (r0_c0=1, r0_c1=2) : False (attendu: False)
Test (r0_c0=2, r0_c1=1) : True (attendu: True)

Interprétation : Produit de contraintes

Sortie obtenue :

MDD de la ligne 2×2 : 7 nœuds
MDD de la contrainte r0_c0 != 1 : visualisé — la branche 1 mène à INVALID, la branche 2 à VALID
MDD produit (ligne INTERSECT contrainte) : 5 nœuds, et les deux tests sémantiques conformes aux valeurs attendues

Le résultat contre-intuitif est là : croiser la ligne avec une contrainte supplémentaire rend le diagramme plus petit — 5 nœuds, contre 7 pour la ligne seule. Le produit (intersection) ne concatène pas les deux structures : il les fusionne niveau par niveau puis réduit le résultat. Le chemin r0_c0 = 1, rejeté par la contrainte, est coupé à la racine, et tout ce qu’il portait disparaît avec lui. Ajouter une contrainte retire des chemins de l’espace de recherche au lieu d’ajouter de la structure.

Les deux tests le vérifient sémantiquement : (r0_c0=1, r0_c1=2) rend False — l’affectation formerait une ligne valide, mais la contrainte dédiée la rejette — tandis que (r0_c0=2, r0_c1=1) rend True. C’est exactement l’opération au cœur de la propagation de contraintes : chaque contrainte ajoute des coupes, et le produit accumule ces coupes en une structure unique. Sur une grille 2×2 l’économie est symbolique ; c’est ce mécanisme qui, enchaîné sur les 27 contraintes d’un Sudoku complet, remplacerait l’énumération exhaustive — au prix de l’explosion documentée en section 4.

6. Solveur Sudoku avec MDD (20 min)

6.1 Architecture du Solveur

Pour résoudre un Sudoku complet avec MDD, nous devrions théoriquement: 1. Construire 27 MDD (9 lignes + 9 colonnes + 9 blocs) 2. Faire le produit des 27 MDD 3. Chercher un chemin valide dans le MDD résultant

Problème : Le MDD résultant serait gigantesque!

6.2 Approche Pragmatique

Nous allons utiliser une approche hybride : - Utiliser les MDD pour vérifier les contraintes localement - Utiliser le backtracking pour la recherche globale

using System;
using System.Collections.Generic;
using System.Linq;

/// <summary>
/// Solveur Sudoku utilisant des MDD pour la vérification de contraintes.
/// Contrairement à Z3, les MDD vérifient les contraintes par parcours
/// de graphe plutôt que par SAT solving.
/// </summary>
public class SudokuMDDSolver
{
    private int[,] _grid;
    private List<MDDNode> _constraintMDDs;
    
    public SudokuMDDSolver(string puzzle)
    {
        _grid = ParsePuzzle(puzzle);
        _constraintMDDs = new List<MDDNode>();
        BuildConstraintMDDs();
    }

    private int[,] ParsePuzzle(string puzzle)
    {
        int[,] grid = new int[9, 9];
        int idx = 0;
        foreach (char c in puzzle.Replace(".", "0"))
        {
            if (char.IsDigit(c) && idx < 81)
            {
                grid[idx / 9, idx % 9] = c - '0';
                idx++;
            }
        }
        return grid;
    }

    /// <summary>
    /// Construit les MDD pour les contraintes de ligne, colonne, bloc.
    /// Note: On construit des MDD simplifiés pour éviter l'explosion.
    /// </summary>
    private void BuildConstraintMDDs()
    {
        // Pour une vraie approche MDD pure, on construirait 27 MDD complets.
        // Ici, on utilise une version simplifiée pour la démonstration.
        
        // Pour chaque ligne, on vérifie que les valeurs sont distinctes
        // en utilisant une méthode directe plus efficace que le MDD complet.
    }

    /// <summary>
    /// Vérifie si une valeur est valide pour une cellule (contraintes MDD).
    /// </summary>
    private bool IsValid(int row, int col, int value)
    {
        // Vérifie la ligne
        for (int j = 0; j < 9; j++)
            if (j != col && _grid[row, j] == value)
                return false;
        
        // Vérifie la colonne
        for (int i = 0; i < 9; i++)
            if (i != row && _grid[i, col] == value)
                return false;
        
        // Vérifie le bloc 3x3
        int blockRow = (row / 3) * 3;
        int blockCol = (col / 3) * 3;
        for (int i = blockRow; i < blockRow + 3; i++)
            for (int j = blockCol; j < blockCol + 3; j++)
                if ((i != row || j != col) && _grid[i, j] == value)
                    return false;
        
        return true;
    }

    /// <summary>
    /// Résout le Sudoku avec backtracking.
    /// </summary>
    public int[,] Solve()
    {
        if (SolveRecursive(0, 0))
            return _grid;
        return null;
    }

    private bool SolveRecursive(int row, int col)
    {
        // Cellule suivante
        if (col >= 9)
        {
            row++;
            col = 0;
            if (row >= 9)
                return true; // Solution trouve
        }

        // Si la cellule est déjà remplie, passer à la suivante
        if (_grid[row, col] != 0)
            return SolveRecursive(row, col + 1);

        // Essayer chaque valeur possible
        for (int value = 1; value <= 9; value++)
        {
            if (IsValid(row, col, value))
            {
                _grid[row, col] = value;
                if (SolveRecursive(row, col + 1))
                    return true;
                _grid[row, col] = 0; // Backtrack
            }
        }

        return false;
    }
}

Console.WriteLine("Classe SudokuMDDSolver definie avec succes.");
Console.WriteLine("Note: Cette implementation utilise le backtracking classique");
Console.WriteLine("car les MDD complets pour Sudoku seraient trop volumineux.");

Classe SudokuMDDSolver definie avec succes.
Note: Cette implementation utilise le backtracking classique
car les MDD complets pour Sudoku seraient trop volumineux.

6.3 Test du Solveur

Notons que ce solveur est essentiellement du backtracking. La vraie valeur de l’approche MDD serait dans la composition de contraintes, mais l’explosion d’états la rend impraticable pour Sudoku complet.

Interprétation : Solveur MDD

Sortie obtenue : Le solveur trouve la solution, mais avec des performances similaires au backtracking classique.

Temps de résolution : moins d’une milliseconde sur le puzzle facile testé ((mesure, voir cellule precedente) — valeur ponctuelle indicative, var d’une machine à l’autre).

Point important : Bien que nous ayons construit des MDD pour illustrer la théorie, l’approche pratique pour Sudoku utilise le backtracking direct. Les MDD brillent vraiment pour des contraintes plus locales ou des problèmes de vérification.

Note (mandat #9377/#9434) : la durée wall-clock (0,46 ms) est machine-dépendante par construction (compile .NET + JIT + GC, charge CPU du runner) et drainée au profit d’un référal à la cellule de mesure amont. La tendance qualitative (ordre de grandeur < 1 ms sur grille facile) est reproductible et conservée en prose. La mesure exacte reste visible dans la cellule de code immédiatement précédente (sortie Kernel.Elapsed / Stopwatch).

Exercice : Comparer les performances BDD vs MDD

Objectif : Comparez les performances des solveurs BDD et MDD sur des puzzles de différentes difficultés en mesurant le temps et la taille des structures.

Indice : Mesurez la taille (nombre de nœuds) et le temps de construction et de résolution.

// EXERCICE : Comparer les performances BDD vs MDD
public Dictionary<string, (double TimeMs, int NodeCount)> CompareBDDvsMDD(int[,] puzzle)
{
    // TODO: Construisez les structures BDD et MDD pour le même puzzle
    // et comparez les temps de construction et résolution
    return null; // TODO etudiant
}
Console.WriteLine("Exercice a completer");

Exercice a completer

using System.Diagnostics;

void DisplayGrid(int[,] grid)
{
    Console.WriteLine("-------+-------+-------");
    for (int i = 0; i < 9; i++)
    {
        if (i > 0 && i % 3 == 0)
            Console.WriteLine("-------+-------+-------");
        
        for (int j = 0; j < 9; j++)
        {
            if (j > 0 && j % 3 == 0)
                Console.Write("| ");
            Console.Write($"{grid[i, j]} ");
        }
        Console.WriteLine();
    }
    Console.WriteLine("-------+-------+-------");
}

string easyPuzzle = "003020600900305001001806400008102900700000008006708200002609500800203009005010300";

Console.WriteLine("=== Puzzle Sudoku Facile ===");
var solver = new SudokuMDDSolver(easyPuzzle);

var stopwatch = Stopwatch.StartNew();
int[,] solution = solver.Solve();
stopwatch.Stop();

if (solution != null)
{
    Console.WriteLine($"\nSolution trouve en {stopwatch.Elapsed.TotalMilliseconds:F2} ms :");
    DisplayGrid(solution);
}
else
{
    Console.WriteLine("\nAucune solution trouvee.");
}

=== Puzzle Sudoku Facile ===

Solution trouve en 1,27 ms :
-------+-------+-------
4 8 3 | 9 2 1 | 6 5 7 
9 6 7 | 3 4 5 | 8 2 1 
2 5 1 | 8 7 6 | 4 9 3 
-------+-------+-------
5 4 8 | 1 3 2 | 9 7 6 
7 2 9 | 5 6 4 | 1 3 8 
1 3 6 | 7 9 8 | 2 4 5 
-------+-------+-------
3 7 2 | 6 8 9 | 5 1 4 
8 1 4 | 2 5 3 | 7 6 9 
6 9 5 | 4 1 7 | 3 8 2 
-------+-------+-------

7. Comparaison Sudoku-12 vs Sudoku-14 (10 min)

7.1 Tableau Comparatif

Aspect	Sudoku-12 (Z3)	Sudoku-14 (BDD/MDD)
Théorie	Automates compilés vers SMT	Vrais automates avec états
Structure	Variables Z3 + contraintes	Graphe de décision
Opérations	Conjonction de contraintes	Produit d’automates
Vérification	SAT solving	Parcours de graphe
Performance	(mesure, voir cellule precedente)	(mesure, voir cellule precedente)
Authenticité	⭐⭐ Approche hybride	⭐⭐⭐ Vrais automates
Pragmatisme	⭐⭐⭐ Production-ready	⭐ Théorique

7.2 Quand Utiliser Chaque Approche

Situation	Approche	Pourquoi
Production	Z3 (Sudoku-12)	Performance optimale
Apprentissage théorie	BDD/MDD (Sudoku-14)	Comprendre les automates
Vérification formelle	BDD	Model checking
Problèmes CSP	Z3 ou OR-Tools	Meilleur scaling

7.3 Conclusion

Les deux notebooks sont complémentaires : - Sudoku-12 montre comment les concepts d’automates se compilent vers Z3 - Sudoku-14 montre l’approche pure avec BDD/MDD

Laquelle est “meilleure”? Dépendez de votre objectif : - Pour résoudre des Sudoku : Z3 - Pour comprendre la théorie : BDD/MDD

Note (mandat #9377/#9434) : les durées wall-clock de cette table comparative sont machine-dépendantes par construction et drainées. Le rapport d’ordres de grandeur (Z3 ~ 20 ms vs BDD ≈≪ 1 ms sur ce puzzle) est reproductible d’une exécution à l’autre et conservé. Les mesures exactes restent visibles dans les cellules de mesure amont (cellule [24] du notebook Sudoku-12-Z3-CSharp pour la mesure Z3 ; §6 du présent notebook pour la mesure BDD/MDD).

Conclusion

8.1 Résumé

Dans ce notebook, nous avons exploré :

Concept	Description
BDD	Binary Decision Diagram - graphe de décision booléen
MDD	Multi-valued Decision Diagram - généralisation aux domaines finis
Produit d’automates	Intersection des langages par produit de graphes
Réduction	Partage de sous-graphes pour compacité

8.2 Points Clés

Les BDD/MDD sont des structures puissantes pour représenter des fonctions booléennes de manière compacte
Les opérations (AND, OR, produit) sont naturelles sur les BDD
Pour Sudoku, l’explosion d’états rend les MDD complets impraticables
L’approche Z3 (Sudoku-12) est plus pragmatique pour la résolution
Les BDD brillent en model checking et vérification formelle

8.3 Perspectives

Model Checking : Vérification de protocoles, circuits logiques
Synthèse de code : Génération de programmes corrects par construction
Théorie des automates : Automates d’arbres, automates de mots infinis

8.4 Tableau de Synthèse Finale

#	Notebook	Approche	Temps (Easy)	Pureté “automata”
12	SFA + Z3	Compilation vers SMT	(mesure, voir cellule precedente)	⭐
14	BDD/MDD	Automates purs	(mesure, voir cellule precedente)	⭐⭐⭐

Les deux approches ont leur place : l’une pour la pratique, l’autre pour la théorie.

Note (mandat #9377/#9434) : les durées wall-clock (~20 ms, < 1 ms) de cette table de synthèse finale sont machine-dépendantes par construction et drainées. Le rapport d’ordres de grandeur (Z3 ~ 20 ms vs BDD ≈≪ 1 ms sur ce puzzle) est reproductible d’une exécution à l’autre et conservé. Les mesures exactes restent visibles dans les cellules de mesure amont (cellule [24] du notebook Sudoku-12-Z3-CSharp pour la mesure Z3 ; §6 du présent notebook pour la mesure BDD/MDD). La synthèse pédagogique tient sur la discrimination théorique (SFA compilation vs BDD automates purs), pas sur les valeurs quantitatives ponctuelles.

Exercices : BDD et MDD

Exercice 1 : BDD pour x OR y

Construire un BDD pour la fonction x OR y et vérifier qu’il donne les bons résultats pour toutes les combinaisons de x et y.

Exercice 2 : Réduction de BDD

Modifier la méthode Create pour implémenter la réduction complète (partage de tous les sous-graphes identiques, pas juste les terminaux).

Exercice 3 : MDD pour Contrainte de Bloc

Construire un MDD pour un bloc 3x3 (9 cellules avec valeurs distinctes). Comparer la taille avec le MDD de ligne.

Exercice 4 : Produit de Trois MDD

Implémenter le produit de trois MDD (ligne x colonne x bloc) pour une seule cellule. Quelle est la taille du MDD résultant?

Exercice 5 : Comparaison de Performance

Comparer le temps de résolution de Sudoku-12 (Z3) et Sudoku-14 (BDD/MDD) sur les mêmes puzzles. Quelle est la différence?

Exercice : Solveur BDD avec Propagation de Contraintes

Objectif :

Implémenter un solveur Sudoku qui utilise les MDD pour propager les contraintes avant chaque affectation. Contrairement au solveur de la section 6 qui ne fait que vérifier les contraintes, votre solveur devra :

Construire un MDD par contrainte (9 lignes + 9 colonnes + 9 blocs = 27 MDD)
Propagation : Avant d’affecter une valeur à une cellule, filtrer les valeurs incompatibles dans les MDD des contraintes concernées
Arc-cohérence : Maintenir la cohérence d’arc entre les domaines des cellules et les MDD

Specification

Implémenter la classe BDDConstraintPropagator avec : - FilterDomain(row, col, currentDomain) : retourne le domaine filtré par les MDD des contraintes de la cellule - Solve(puzzle) : résout le Sudoku en combinant propagation MDD et backtracking

Critère de succès

Votre solveur doit : - Trouver la même solution que le solveur de référence - Réduire le nombre de retours arrière grâce à la propagation

À retenir

Les BDD/MDD offrent une représentation compacte des fonctions booléennes et des domaines finis :

Un BDD non réduit pour x AND y compte 5 nœuds (cf. cellule 7, où les deux feuilles False ne sont pas fusionnées) ; la réduction BDD partage ces terminaux identiques et descend à 4 nœuds. C’est sur des fonctions plus complexes que ce partage de sous-graphes fait décoller l’avantage du BDD face à une table de vérité exponentielle (2ⁿ lignes).
Le MDD d’une seule ligne Sudoku atteint 5 611 771 nœuds (vs 9! = 362 880 permutations valides) : l’explosion d’états rend les MDD complets impraticables pour Sudoku.
Le solveur MDD est en réalité hybride (backtracking + vérification MDD), résolu en (mesure, voir cellule precedente) sur grille Easy (valeur ponctuelle indicative).
Z3/SMT (Sudoku-12) reste l’approche de production (bitvectors, ordre de grandeur conservé d’une machine à l’autre : voir cellule de mesure amont du notebook Sudoku-12-Z3-CSharp), tandis que les BDD excellent en model checking et vérification formelle.

Note (mandat #9377/#9434) : les durées wall-clock (0,46 ms, 166-470 ms) de cette cellule récapitulative sont machine-dépendantes par construction (compile .NET + JIT + GC, charge CPU du runner) et drainées. Les faits reproductibles (résolution réussie, ordre de grandeur global, existence d’une explosion d’états des MDD) sont conservés. Les mesures exactes restent visibles dans les cellules de mesure amont (cellule [24] du notebook Sudoku-12-Z3-CSharp pour la mesure Z3 bitvector ; cellule de code immédiatement précédente du présent notebook pour la mesure MDD 0,46 ms). Les tailles de graphes (5 611 771 nœuds MDD, 4-5 nœuds BDD) sont déterministes (forme canonique BDD, construction MDD systématique) et non affectées par la dérive machine — elles sont conservées telles quelles.

Références

Bibliographie

Bryant, R. E. - “Graph-Based Algorithms for Boolean Function Manipulation” (1986) - L’article fondateur des BDD
Andersen, H. R. - “An Introduction to Binary Decision Diagrams” (1997) - Tutoriel excellent
Somenzi, F. - “Binary Decision Diagrams” (1999) - Vue d’ensemble complète

Liens

CUDD: CU Decision Diagram Package - Bibliothèque BDD référence
Sylvan: Parallel BDD library - BDD parallèle moderne

Notebooks connexes

Sudoku-13-SymbolicAutomata - Automates compilés vers Z3
Sudoku-12-Z3 - Z3 SMT direct
Search-10-SymbolicAutomata - Théorie approfondie

Navigation : Sudoku README | Sudoku-13-SymbolicAutomata | Fin

Retour au sommaire : Index Sudoku

// À COMPLÉTER : Solveur BDD avec propagation de contraintes

public class BDDConstraintPropagator
{
    private readonly List<MDDNode> _rowMDDs;
    private readonly List<MDDNode> _colMDDs;
    private readonly List<MDDNode> _blockMDDs;

    public BDDConstraintPropagator()
    {
        // TODO étudiant : Construire les 27 MDD (9 lignes + 9 colonnes + 9 blocs)
        // Hint : Utiliser RowMDDBuilder et adapter pour colonnes et blocs
        _rowMDDs = new List<MDDNode>();
        _colMDDs = new List<MDDNode>();
        _blockMDDs = new List<MDDNode>();
    }

    /// <summary>
    /// Filtre le domaine d'une cellule en utilisant les MDD des contraintes.
    /// </summary>
    /// <param name="row">Ligne de la cellule (0-8)</param>
    /// <param name="col">Colonne de la cellule (0-8)</param>
    /// <param name="currentAssignment">Valeurs déjà affectées dans la grille</param>
    /// <param name="currentDomain">Domaine actuel de la cellule {1,...,9}</param>
    /// <returns>Domaine filtre (valeurs compatibles avec les contraintes MDD)</returns>
    public IEnumerable<int> FilterDomain(
        int row, int col,
        Dictionary<string, int> currentAssignment,
        IEnumerable<int> currentDomain)
    {
        // TODO étudiant : Pour chaque valeur candidate, vérifier via les MDD
        // si elle est compatible avec les affectations actuelles
        return currentDomain;  // TODO etudiant : a completer
    }

    /// <summary>
    /// Résout un Sudoku en combinant propagation MDD et backtracking.
    /// </summary>
    public int[,] Solve(string puzzle)
    {
        return null;  // TODO etudiant : a completer
    }
}
Console.WriteLine("BDDConstraintPropagator class defined (exercice a completer)");

// Test : Vérifier que votre solveur trouve la même solution que le solveur de référence
// string puzzle = "003020600900305001001806400008102900700000008006708200002609500800203009005010300";
// var propagator = new BDDConstraintPropagator();
// var solution = propagator.Solve(puzzle);
// Console.WriteLine(solution != null ? "Solution trouvée !" : "Échec !");

BDDConstraintPropagator class defined (exercice a completer)

Retour au sommet