Sudoku-14 : Automates avec BDD/MDD - Approche Pure (Python)

Jumeau Python du notebook Sudoku-14-BDD-CSharp.ipynb. Version .NET (C#) hand-rolled ↔︎ Version Python hand-rolled (parité pédagogique : les deux enseignent les internes des diagrammes de décision, sans librairie BDD). Cf marathon parité .NET ⇄ Python (#4956).

Qu’est-ce qu’un BDD ?

Un BDD (Binary Decision Diagram) est une structure de données compacte pour représenter une fonction booléenne. C’est un graphe orienté acyclique où :

• Chaque nœud interne teste une variable booléenne (x?).
• Deux branches sortent : False (bas) et True (haut).
• Les feuilles sont True ou False.

Un MDD (Multi-valued Decision Diagram) généralise le BDD : chaque nœud teste une variable à plusieurs valeurs (ex : une cellule de Sudoku ∈ {1..9}).

Objectifs d’apprentissage

1. Comprendre la structure d’un BDD et son fonctionnement.
2. Implémenter un BDD simple en Python (avec réduction).
3. Définir des opérations sur les BDD (AND, OR, NOT via Apply).
4. Construire un MDD pour la contrainte « 9 valeurs distinctes par ligne ».
5. Combiner les MDD (produit) pour modéliser le Sudoku complet.

Prérequis

• Notions de structures de données (arbres, graphes).
• Python 3.10+ (typing, dataclasses).

Durée estimée : 25 min

Références

• Bryant, R. E. (1986). Graph-Based Algorithms for Boolean Function Manipulation.
• Andersen, H. R. (1997). An Introduction to Binary Decision Diagrams.
• Notebook C# associé : Sudoku-14-BDD-CSharp.ipynb.

1. Introduction - BDD vs Z3 (10 min)

1.1 Comparaison des Approches

Approche	Outil	Type	Avantage	Inconvénient
SMT/SAT	Z3 (Sudoku-12)	Solveur générique	Expressif, contraintes arbitraires	Lourd, boîte noire
BDD/MDD	Hand-rolled (ce notebook)	Structure de données explicite	Contrôle total, pédagogique	Pas de réduction canonique complète

1.2 Pourquoi BDD ?

Le BDD offre une représentation canonique (modulo l’ordre des variables) d’une fonction booléenne : deux fonctions équivalentes ont le même BDD réduit. Cela permet de tester l’équivalence et la satisfiabilité en temps linéaire.

1.3 MDD pour Sudoku

Pour le Sudoku, on manipule des variables à 9 valeurs (les chiffres 1-9). Le MDD est l’extension naturelle : un nœud MDD a une branche par valeur possible. On construit un MDD par contrainte (ligne, colonne, bloc), puis on les combine.

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

2.1 Structure du BDD

Nous définissons un nœud BDD comme une classe immuable (@dataclass(frozen=True)) avec deux formes : terminale (feuille True/False) ou interne (variable + deux enfants). L’immuabilité + frozen=True rend les nœuds hashables, ce qui permet la mémoïsation (computed table) dans les opérations.

La réduction de base : si les deux enfants sont identiques, le nœud est inutile → on retourne l’enfant directement.

from __future__ import annotations
from dataclasses import dataclass
from typing import Optional


@dataclass(frozen=True)
class BDDNode:
    """Nœud d'un BDD (Binary Decision Diagram).

    Forme terminale  : variable=None, value∈{True,False}, enfants=None.
    Forme interne    : variable=str, child_false/child_true=BDDNode, value=None.
    """

    variable: Optional[str] = None
    child_false: Optional["BDDNode"] = None
    child_true: Optional["BDDNode"] = None
    value: Optional[bool] = None

    @property
    def is_terminal(self) -> bool:
        return self.variable is None

    @staticmethod
    def create(variable: str, child_false: "BDDNode", child_true: "BDDNode") -> "BDDNode":
        # Réduction : si les deux enfants sont identiques, retourner l'enfant.
        if child_false == child_true:
            return child_false
        return BDDNode(variable=variable, child_false=child_false, child_true=child_true)

    def evaluate(self, assignment: dict[str, bool]) -> bool:
        """Évalue le BDD pour une assignation de variables."""
        if self.is_terminal:
            assert self.value is not None
            return self.value
        var_value = assignment.get(self.variable, False)
        child = self.child_true if var_value else self.child_false
        assert child is not None
        return child.evaluate(assignment)

    def count_nodes(self) -> int:
        """Compte le nombre de nœuds (uniques par référence) dans le BDD."""
        if self.is_terminal:
            return 1
        assert self.child_false is not None and self.child_true is not None
        return 1 + self.child_false.count_nodes() + self.child_true.count_nodes()

    def pretty(self, indent: str = "") -> str:
        if self.is_terminal:
            return f"{indent}({self.value})"
        assert self.child_false is not None and self.child_true is not None
        lines = [f"{indent}{self.variable}?"]
        lines.append(f"{indent}  |-> {self.child_true.pretty(indent + '  |').strip()}")
        lines.append(f"{indent}  |-> {self.child_false.pretty(indent + '  |').strip()}")
        return "\n".join(lines)

    def __str__(self) -> str:
        return self.pretty()


# Terminaux (singletons immuables/hashables).
BDD_TRUE = BDDNode(value=True)
BDD_FALSE = BDDNode(value=False)

print("Classe BDDNode définie avec succès.")
print("Opérations disponibles :")
print("  - BDD_TRUE / BDD_FALSE : Terminaux (feuilles)")
print("  - BDDNode.create(var, low, high) : Crée un nœud de décision")
print("  - node.evaluate(assign) : Évalue le BDD")
print("  - node.count_nodes() : Compte les nœuds")

Classe BDDNode définie avec succès.
Opérations disponibles :
  - BDD_TRUE / BDD_FALSE : Terminaux (feuilles)
  - BDDNode.create(var, low, high) : Crée un nœud de décision
  - node.evaluate(assign) : Évalue le BDD
  - node.count_nodes() : Compte les nœuds

Anatomie du BDDNode : deux terminaux, un type de nœud

Un BDD (diagramme de décision binaire) n’a que deux sortes de nœuds, et la sortie les énumère : les terminaux BDD_TRUE / BDD_FALSE (les feuilles — la réponse) et les nœuds de décision créés par BDDNode.create(var, low, high) : tester la variable var, descendre vers low si elle est fausse, vers high si elle est vraie. C’est tout. La puissance vient du partage : create est une opération d’interning — deux nœuds de même (var, low, high) sont physiquement le même objet, ce qui transforme l’arbre de décision (exponentiel) en DAG (souvent compact). count_nodes() mesurera ce que l’arbre aurait dû être en DAG — le décompte des tests suivants en fera la démonstration chiffrée.

Une précision structurante pour la suite : la compacité d’un BDD dépend de l’ordre des variables — deux ordres différents peuvent donner quelques nœuds ou exponentiellement plus pour la même fonction. Les implémentations industrielles (CUDD, dd) réordonnent dynamiquement ; ici l’ordre est fixe, et c’est un paramètre à garder en tête quand les comptes de nœuds des sections suivants sembleront étonnamment compacts (ou non).

Exercice 1 : Construire un BDD pour la contrainte « exactement un parmi N »

Construisez un BDD qui est vrai si et exactement si une seule des N variables booléennes données est vraie.

# EXERCICE : Construire un BDD pour la contrainte "exactement un parmi N"
def exactly_one_of_n(variables: list[str]) -> BDDNode:
    # TODO etudiant : Construisez un BDD qui est vrai si exactement une
    # des N variables est vraie.
    # Indice : parcourez les variables ; à chaque étape, suivez deux états
    #   (a) aucune variable vraie jusqu'ici  (b) exactement une déjà vraie.
    # Etape 1 : cas de base (0 variables) -> FALSE.
    # Etape 2 : récursion sur la variable courante selon l'état.
    # Etape 3 : combinez via BDDNode.create.
    return None  # TODO etudiant


print("Exercice à compléter (ExactlyOneOfN).")

Exercice à compléter (ExactlyOneOfN).

2.2 Exemples de BDD

Trois exemples : la constante TRUE, une variable simple x, et x AND y.

# Exemple 1 : BDD pour la fonction constante TRUE
bdd_true = BDD_TRUE
print("=== Exemple 1 : Constante TRUE ===")
print(f"Noeuds : {bdd_true.count_nodes()}")
print(f"Valeur : {bdd_true.evaluate({})}")
print()

# Exemple 2 : BDD pour une variable simple x
bdd_x = BDDNode.create("x", BDD_FALSE, BDD_TRUE)
print("=== Exemple 2 : Variable x ===")
print(bdd_x)
print(f"Noeuds : {bdd_x.count_nodes()}")
print(f"Eval(x=True)  : {bdd_x.evaluate({'x': True})}")
print(f"Eval(x=False) : {bdd_x.evaluate({'x': False})}")
print()

# Exemple 3 : BDD pour x AND y
# x AND y = si x False -> False ; si x True -> résultat = y
bdd_y = BDDNode.create("y", BDD_FALSE, BDD_TRUE)
bdd_x_and_y = BDDNode.create("x", BDD_FALSE, bdd_y)
print("=== Exemple 3 : x AND y ===")
print(bdd_x_and_y)
print(f"Noeuds : {bdd_x_and_y.count_nodes()}")
print(f"Eval(x=True, y=True)  : {bdd_x_and_y.evaluate({'x': True, 'y': True})}")
print(f"Eval(x=True, y=False) : {bdd_x_and_y.evaluate({'x': True, 'y': False})}")
print(f"Eval(x=False, y=True) : {bdd_x_and_y.evaluate({'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

• Constante TRUE : un seul nœud (la feuille True). Aucune variable à tester.
• Variable x : 3 nœuds (la racine x? et les deux feuilles True et False). Le chemin True mène à True, le chemin False mène à False.
• x AND y : 5 nœuds (comptage par référence : la feuille False est atteinte par deux chemins, donc comptée deux fois). On voit la factorisation : quand x est False, on retourne directement False sans tester y (court-circuit). C’est l’avantage du BDD sur la table de vérité (4 lignes) : représentation compacte.

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

3.1 Opération AND (Apply)

L’opération clé est Apply : étant donné deux BDD f et g et un opérateur booléen op (AND, OR, XOR…), construire le BDD de op(f, g).

Algorithme récursif avec mémoïsation (computed table) : - Si f et g sont terminaux : appliquer op directement. - Sinon : prendre la variable de plus haut niveau (la plus petite dans l’ordre fixé), récursion sur les deux branches.

La mémoïsation évite de recalculer les sous-problèmes déjà résolus. L’ordre des variables est ici l’ordre lexicographique des noms ("x" < "y" < "z").

class BDDOperations:
    """Opérations sur les BDD : Apply (op binaire), And/Or/Not.
    Version pédagogique : réduction locale via BDDNode.create."""

    # Cache (computed table) : (f, g, op_name) -> résultat.
    # f, g sont hashables (BDDNode frozen=True).
    _cache: dict[tuple, BDDNode] = {}

    @classmethod
    def _clear_cache(cls) -> None:
        cls._cache.clear()

    @classmethod
    def apply(cls, f: BDDNode, g: BDDNode, op, op_name: str) -> BDDNode:
        """Applique un opérateur booléen sur deux BDD."""
        # Terminal / terminal.
        if f.is_terminal and g.is_terminal:
            assert f.value is not None and g.value is not None
            return BDD_TRUE if op(f.value, g.value) else BDD_FALSE

        # Mémoïsation.
        key = (f, g, op_name)
        if key in cls._cache:
            return cls._cache[key]

        # Déterminer la variable de tête (plus petite dans l'ordre lexicographique).
        f_var = None if f.is_terminal else f.variable
        g_var = None if g.is_terminal else g.variable
        if f_var is not None and (g_var is None or f_var < g_var):
            top = f_var
            f_lo, f_hi = f.child_false, f.child_true
            g_lo = g_hi = g
        elif g_var is not None and (f_var is None or g_var < f_var):
            top = g_var
            g_lo, g_hi = g.child_false, g.child_true
            f_lo = f_hi = f
        else:  # f_var == g_var (et non None).
            top = f_var
            f_lo, f_hi = f.child_false, f.child_true
            g_lo, g_hi = g.child_false, g.child_true

        assert top is not None and f_lo is not None and f_hi is not None
        res_lo = cls.apply(f_lo, g_lo, op, op_name)
        res_hi = cls.apply(f_hi, g_hi, op, op_name)
        result = BDDNode.create(top, res_lo, res_hi)
        cls._cache[key] = result
        return result

    @classmethod
    def and_(cls, f: BDDNode, g: BDDNode) -> BDDNode:
        return cls.apply(f, g, lambda a, b: a and b, "AND")

    @classmethod
    def or_(cls, f: BDDNode, g: BDDNode) -> BDDNode:
        return cls.apply(f, g, lambda a, b: a or b, "OR")

    @classmethod
    def not_(cls, f: BDDNode) -> BDDNode:
        # Négation récursive (unop) : on échange les feuilles.
        if f.is_terminal:
            assert f.value is not None
            return BDD_FALSE if f.value else BDD_TRUE
        key = (f, "NOT")
        if key in cls._cache:
            return cls._cache[key]
        assert f.child_false is not None and f.child_true is not None
        result = BDDNode.create(f.variable, cls.not_(f.child_false), cls.not_(f.child_true))
        cls._cache[key] = result
        return result


print("BDDOperations défini : apply / and_ / or_ / not_ (avec computed table).")

BDDOperations défini : apply / and_ / or_ / not_ (avec computed table).

Anatomie d’apply : la table calculée, condition du polynomial

BDDOperations fournit apply (l’opération binaire générique, paramétrée par un opérateur booléen) et ses dérivés and_ / or_ / not_. Le point décisif est entre parenthèses : la table calculée (computed table). apply procède par récursion simultanée sur les deux opérandes et mémoïse chaque résultat intermédiaire — sans elle, la moindre composition re-recalcule des sous-DAG entiers et le coût explose ; avec elle, chaque paire de nœuds est résolue au plus une fois et apply reste polynomiale en la taille des opérandes. C’est le même mécanisme qui rend la manipulation symbolique de contraintes praticable : les tests de la section 3 composent des formules sans jamais développer leurs tables de vérité.

3.2 Test des Opérations

Vérifions les identités booléennes classiques : x AND NOT x = FALSE, x OR NOT x = TRUE, et la distributivité.

BDDOperations._clear_cache()

bdd_x = BDDNode.create("x", BDD_FALSE, BDD_TRUE)

# Test 1 : x AND NOT x = FALSE
bdd_not_x = BDDOperations.not_(bdd_x)
bdd_x_and_not_x = BDDOperations.and_(bdd_x, bdd_not_x)
print("=== Test 1 : x AND NOT x ===")
print(f"Résultat : {bdd_x_and_not_x.evaluate({})}")
print(f"Attendu : False")
print(f"Noeuds : {bdd_x_and_not_x.count_nodes()}")
print()

# Test 2 : x OR NOT x = TRUE
bdd_x_or_not_x = BDDOperations.or_(bdd_x, bdd_not_x)
print("=== Test 2 : x OR NOT x ===")
print(f"Résultat : {bdd_x_or_not_x.evaluate({})}")
print(f"Attendu : True")
print(f"Noeuds : {bdd_x_or_not_x.count_nodes()}")
print()

# Test 3 : (x AND y) OR (x AND z) = x AND (y OR z)   (distributivité)
bdd_y = BDDNode.create("y", BDD_FALSE, BDD_TRUE)
bdd_z = BDDNode.create("z", BDD_FALSE, BDD_TRUE)
bdd_left = BDDOperations.or_(BDDOperations.and_(bdd_x, bdd_y),
                             BDDOperations.and_(bdd_x, bdd_z))
bdd_right = BDDOperations.and_(bdd_x, BDDOperations.or_(bdd_y, bdd_z))

print("=== Test 3 : Distributivité ===")
print(f"Noeuds (gauche) : {bdd_left.count_nodes()}")
print(f"Noeuds (droite) : {bdd_right.count_nodes()}")
assign = {"x": True, "y": True, "z": False}
lg = bdd_left.evaluate(assign)
rg = bdd_right.evaluate(assign)
print(f"Équivalent (x=T,y=T,z=F) : {lg} == {rg}")
# Vérif équivalence sur les 8 assignations.
all_equiv = all(
    bdd_left.evaluate({"x": a, "y": b, "z": c}) == bdd_right.evaluate({"x": a, "y": b, "z": c})
    for a in (False, True) for b in (False, True) for c in (False, True)
)
print(f"Équivalence sur les 8 assignations : {all_equiv}")

=== Test 1 : x AND NOT x ===
Résultat : False
Attendu : False
Noeuds : 1

=== Test 2 : x OR NOT x ===
Résultat : True
Attendu : True
Noeuds : 1

=== Test 3 : Distributivité ===
Noeuds (gauche) : 7
Noeuds (droite) : 7
Équivalent (x=T,y=T,z=F) : True == True
Équivalence sur les 8 assignations : True

Lecture des tests : des tautologies réduites à un seul nœud

Trois résultats, trois leçons. Test 1 : x AND NOT x s’évalue en False avec 1 nœud — l’application de l’opérateur détecte la contradiction au niveau des terminaux et renvoie directement la feuille : à aucun moment un arbre n’est développé, c’est du calcul symbolique, pas de l’énumération. Test 2 : x OR NOT x, symétriquement, donne True sur 1 nœud. Test 3 (distributivité) : les deux expressions de la loi distributive occupent 7 nœuds chacune et sont vérifiées équivalentes — d’abord sur une assignation témoin, puis sur les 8 assignations exhaustives des trois variables. Notez la limite de cette vérification : l’équivalence par évaluation est exponentielle en le nombre de variables — praticable à 3 variables, pas à 81 cellules de Sudoku ; l’équivalence structurelle (DAG identiques après canonisation) est ce qui la remplacera à grande échelle. L’equivalence structurelle est aussi ce qui rendra le comptage de noeuds significatif : deux formules equivalentes, deux DAG de meme taille canonique.

4. MDD pour Sudoku (20 min)

4.1 De BDD à MDD

Un MDD (Multi-valued Decision Diagram) généralise le BDD : chaque nœud teste une variable à plusieurs valeurs. Pour le Sudoku, chaque cellule ∈ {1..9}, donc un nœud MDD a jusqu’à 9 branches sortantes.

On conserve l’égalité structurelle (@dataclass(eq=True)) pour la réduction, mais sans frozen (les MDD ne sont pas utilisés comme clés de cache : la mémoïsation porte sur les entiers (col, masque)).

Anatomie du RowMDDBuilder : la frontière est un masque de bits

La construction du MDD « toutes valeurs distinctes » procède cellule par cellule, et son état de contrôle est un masque de bits des valeurs déjà utilisées : après avoir placé k valeurs distinctes, les seules transitions légales vers la cellule suivante sont les bits non encore posés. C’est pourquoi le MDD d’une ligne de taille N reste modeste : la frontière utile compte au plus 2^N sous-ensembles, massivement partagés entre chemins qui ont utilisé le même ensemble de valeurs dans des ordres différents — deux ordres différents des mêmes valeurs convergent vers le même nœud, c’est le partage qui comprime. Un BDD binaire (une variable booléenne par couple cellule-valeur) devrait lui distinguer les ordres : c’est l’avantage structurel du MDD multi-valué pour les contraintes toutes-différentes.

@dataclass
class MDDNode:
    """Nœud d'un MDD (Multi-valued Decision Diagram) pour Sudoku.

    Forme terminale : cell_name=None, is_valid∈{True,False}, children=None.
    Forme interne   : cell_name=str, children=dict[int, MDDNode].
    """

    cell_name: Optional[str] = None
    children: Optional[dict] = None
    is_terminal_flag: bool = False
    is_valid: bool = False

    @property
    def is_terminal(self) -> bool:
        return self.is_terminal_flag

    @staticmethod
    def create(cell_name: str, children: dict) -> "MDDNode":
        if len(children) == 0:
            return MDDNode(is_terminal_flag=True, is_valid=False)
        first = next(iter(children.values()))
        # Réduction simple : tous les enfants identiques -> retourner l'enfant.
        if all(c == first for c in children.values()):
            return first
        # Tous invalides -> INVALID.
        invalid = MDDNode(is_terminal_flag=True, is_valid=False)
        if all(c == invalid for c in children.values()):
            return invalid
        return MDDNode(cell_name=cell_name, children=dict(children))

    def evaluate(self, assignment: dict[str, int]) -> bool:
        if self.is_terminal:
            return self.is_valid
        if self.cell_name not in assignment:
            return False
        v = assignment[self.cell_name]
        assert self.children is not None
        if v not in self.children:
            return False
        return self.children[v].evaluate(assignment)

    def count_nodes(self) -> int:
        if self.is_terminal:
            return 1
        assert self.children is not None
        return 1 + sum(c.count_nodes() for c in self.children.values())

    def pretty(self, indent: str = "") -> str:
        if self.is_terminal:
            return f"{indent}({'VALID' if self.is_valid else 'INVALID'})"
        assert self.children is not None
        lines = [f"{indent}{self.cell_name}?"]
        for k in sorted(self.children.keys()):
            lines.append(f"{indent}  {k} -> {self.children[k].pretty(indent + '  |  ').strip()}")
        return "\n".join(lines)

    def __str__(self) -> str:
        return self.pretty()


# Terminaux.
MDD_VALID = MDDNode(is_terminal_flag=True, is_valid=True)
MDD_INVALID = MDDNode(is_terminal_flag=True, is_valid=False)

print("MDDNode défini (pretty/evaluate/create).")

MDDNode défini (pretty/evaluate/create).

4.2 MDD pour une contrainte de ligne

On construit un MDD pour la contrainte « N valeurs distinctes dans une ligne ». On parcourt les colonnes en mémorisant les valeurs déjà utilisées (masque de N bits). La mémoïsation (col, masque) permet de partager les sous-graphes.

class RowMDDBuilder:
    """Constructeur de MDD pour la contrainte 'ligne = N valeurs distinctes'.
    Mémoïsation via (col, used_mask) pour partager les sous-graphes."""

    def __init__(self, row_index: int, size: int = 9) -> None:
        self.row_index = row_index
        self.size = size
        self._memo: dict[tuple[int, int], MDDNode] = {}

    def build(self) -> MDDNode:
        return self._build_recursive(0, 0)

    def _build_recursive(self, col: int, used_mask: int) -> MDDNode:
        if col >= self.size:
            return MDD_VALID

        key = (col, used_mask)
        if key in self._memo:
            return self._memo[key]

        cell_name = f"r{self.row_index}_c{col}"
        children: dict[int, MDDNode] = {}

        for v in range(1, self.size + 1):
            bit = 1 << (v - 1)
            if used_mask & bit:
                # Valeur déjà utilisée -> branche invalide.
                children[v] = MDD_INVALID
            else:
                children[v] = self._build_recursive(col + 1, used_mask | bit)

        result = MDDNode.create(cell_name, children)
        self._memo[key] = result
        return result


print("RowMDDBuilder défini (N valeurs distinctes via masque de bits + mémoïsation).")

RowMDDBuilder défini (N valeurs distinctes via masque de bits + mémoïsation).

4.3 Test du MDD de ligne

Construisons un MDD de ligne sur une grille 3×3 (3 cellules, valeurs 1-3) pour visualiser la structure sans explosion combinatoire. Le principe est identique à une ligne 9×9 ; seules les branches sont moins nombreuses. La résolution d’une grille 9×9 complète est traitée au §6 (propagation de domaines, plus efficace que la construction explicite du MDD 9×9).

# Construction du MDD pour la ligne 0 sur une grille 3x3 (3 valeurs distinctes).
builder = RowMDDBuilder(row_index=0, size=3)
mdd_line0 = builder.build()
print(f"MDD ligne 0 (3x3) construit : {mdd_line0.count_nodes()} nœuds comptés")
print(f"  (le compte somme les références partagées ; le DAG unique est plus petit)")
print()

# Assignation valide : 3 valeurs distinctes.
valid_row = {"r0_c0": 1, "r0_c1": 2, "r0_c2": 3}
print(f"Ligne valide   [1,2,3] : {mdd_line0.evaluate(valid_row)}  (attendu True)")

# Assignation invalide : doublon (deux fois le 2).
invalid_row2 = {"r0_c0": 2, "r0_c1": 2, "r0_c2": 3}
print(f"Ligne invalide [2,2,3] : {mdd_line0.evaluate(invalid_row2)}  (attendu False)")

MDD ligne 0 (3x3) construit : 31 nœuds comptés
  (le compte somme les références partagées ; le DAG unique est plus petit)

Ligne valide   [1,2,3] : True  (attendu True)
Ligne invalide [2,2,3] : False  (attendu False)

Lecture du MDD ligne : 31 nœuds, et un prédicat exécutable

Le MDD (multi-valued decision diagram) de la contrainte « ligne valide » sur une ligne 3x3 est construit en 31 nœuds comptés — avec la précision honnête de la sortie : le comptage somme des références partagées, le DAG unique est plus petit. Puis le test : [1,2,3] accepté (True), [2,2,3] rejeté (False) — l’automate se traverse en O(longueur de la ligne) pour dire si une affectation de la ligne respecte « toutes distinctes ». C’est le changement de représentation central du notebook : la contrainte n’est plus une formule à démontrer mais un langage reconnu par un automate — et le solveur de la section 6 combinera ces automates par produit pour reconnaître les grilles valides.

Projetez l’échelle : à 3 valeurs la frontière compte au plus 2^3 = 8 sous-ensembles ; à 9 valeurs, 2^9 = 512 — c’est le plafond théorique du nombre d’états de la ligne 9x9, et le partage réel le maintient très en dessous. C’est ce plafond polynomial-en-pratique qui rend le solveur MDD complet de la section 6 praticable (mesuré là-bas : 1,4 ms).

Exercice 2 : Construire un MDD pour la contrainte « tous différents » sur une colonne

Le MDD ci-dessus code « tous différents sur une ligne ». Generalisez-le pour une colonne (cellules r0_cX, r1_cX, ... selon la même dimension).

# EXERCICE : Construire un MDD pour la contrainte "tous différents" sur une colonne
def build_column_mdd(col_index: int, size: int = 9) -> MDDNode:
    # TODO etudiant : adaptez RowMDDBuilder pour une colonne (cellules r{i}_c{col_index}).
    # Indice : le seul changement est le nommage des cellules (r{i}_c{col_index}
    #   au lieu de r{row_index}_c{j}).
    # Etape 1 : créer un builder paramétré par l'axe (ligne vs colonne).
    # Etape 2 : itérer sur l'autre dimension avec le même masque de bits.
    # Etape 3 : réutiliser la mémoïsation (position, used_mask).
    return None  # TODO etudiant


print("Exercice à compléter (MDD colonne).")

Exercice à compléter (MDD colonne).

5. Produit d’Automates explicite (15 min)

5.1 Produit de MDD

Pour modéliser un Sudoku complet, il faut combiner 27 contraintes (9 lignes + 9 colonnes + 9 blocs). L’opération de produit de deux MDD f et g produit un MDD qui accepte une assignation ssi f ET g l’acceptent.

On travaille ici sur une grille 2×2 (valeurs 1-2) pour garder le produit explicite gérable (le produit complet 9×9 serait trop gros sans réduction canonique complète, hors de portée de ce notebook d’introduction).

def mdd_product(f: MDDNode, g: MDDNode, size: int = 9) -> MDDNode:
    """Produit explicite de deux MDD : accepte ssi f ET g acceptent.
    Version pédagogique (grille 2x2) — suppose un ordre commun des cellules."""
    # Terminaux.
    if f.is_terminal and g.is_terminal:
        return MDD_VALID if (f.is_valid and g.is_valid) else MDD_INVALID
    if f.is_terminal:
        # f terminal : INVALID court-circuite (AND) ; VALID => il reste a verifier g.
        return MDD_INVALID if not f.is_valid else g
    if g.is_terminal:
        # symetrique : g INVALID court-circuite ; g VALID => il reste a verifier f.
        return MDD_INVALID if not g.is_valid else f

    assert f.children is not None and g.children is not None
    # Si les deux MDD testent la même cellule, on fusionne les branches.
    if f.cell_name == g.cell_name:
        children: dict[int, MDDNode] = {}
        for v in range(1, size + 1):
            fc = f.children.get(v, MDD_INVALID)
            gc = g.children.get(v, MDD_INVALID)
            children[v] = mdd_product(fc, gc, size)
        return MDDNode.create(f.cell_name, children)
    # Cellules différentes : on avance sur f en propagant g (simplification
    # pédagogique ; suppose que f est "en avance" sur g dans l'ordre des cellules).
    children = {}
    for v, fchild in f.children.items():
        children[v] = mdd_product(fchild, g, size)
    return MDDNode.create(f.cell_name, children)


print("mdd_product défini (produit explicite, fusion sur cellule commune).")

mdd_product défini (produit explicite, fusion sur cellule commune).

5.2 Test du produit

Grille 2×2 (valeurs 1-2) : ligne0 = valeurs distinctes, ligne1 = valeurs distinctes. Le produit exige que les deux lignes soient valides simultanément.

# Grille 2x2 : valeurs {1,2}, chaque ligne doit avoir 2 valeurs distinctes.
SIZE2 = 2

mdd_row0 = RowMDDBuilder(row_index=0, size=SIZE2).build()
mdd_row1 = RowMDDBuilder(row_index=1, size=SIZE2).build()
mdd_grid2 = mdd_product(mdd_row0, mdd_row1, size=SIZE2)

print(f"MDD ligne 0 (size=2) : {mdd_row0.count_nodes()} nœuds")
print(f"MDD ligne 1 (size=2) : {mdd_row1.count_nodes()} nœuds")
print(f"MDD produit 2x2      : {mdd_grid2.count_nodes()} nœuds")
print()

# Assignation valide : deux lignes valides.
valid = {"r0_c0": 1, "r0_c1": 2, "r1_c0": 2, "r1_c1": 1}
print(f"Grille valide    {{1,2}},{{2,1}} : {mdd_grid2.evaluate(valid)}  (attendu True)")

# Assignation invalide : ligne 0 a un doublon.
invalid = {"r0_c0": 1, "r0_c1": 1, "r1_c0": 2, "r1_c1": 1}
print(f"Grille invalide  {{1,1}},{{2,1}} : {mdd_grid2.evaluate(invalid)}  (attendu False)")

MDD ligne 0 (size=2) : 7 nœuds
MDD ligne 1 (size=2) : 7 nœuds
MDD produit 2x2      : 19 nœuds

Grille valide    {1,2},{2,1} : True  (attendu True)
Grille invalide  {1,1},{2,1} : False  (attendu False)

Lecture du produit : 7 + 7 = 19, pas 49

Deux MDD de ligne à 7 nœuds chacun ; leur produit — l’automate qui reconnaît simultanément les deux contraintes, en fusionnant sur la cellule qu’elles partagent — tient en 19 nœuds. Le produit naïf de deux structures de 7 ferait 49 états ; le partage de sous-chemins communs en élimine plus de la moitié. Le test referme la boucle : la grille {1,2},{2,1} est acceptée, {1,1},{2,1} rejetée (le 1 dupliqué sur la colonne partagée). C’est exactement le mécanisme qui montera à l’échelle du Sudoku complet : 27 contraintes-lignes-colonnes-blocs dont les produits partiels restent compacts précisément parce que les cellules partagées fusionnent au lieu de se multiplier.

6. Solveur Sudoku avec MDD (20 min)

6.1 Architecture du solveur

Plutôt que de construire l’énorme MDD du Sudoku complet (qui nécessiterait une réduction canonique complète hors de portée ici), on adopte une approche pragmatique : propager les contraintes MDD ligne/colonne/bloc comme un filtre sur les domaines des cellules, à la manière d’un solveur CP.

6.2 Approche pragmatique

On représente la grille par les domaines (valeurs possibles) de chaque cellule, et on filtre itérativement les valeurs incompatibles avec les contraintes MDD.

def solve_sudoku_mdd(grid: list[list[int]], size: int = 9) -> bool:
    """Solveur Sudoku pragmatique : propagation de domaines + backtracking MRV.

    1. Fixe les domaines depuis la grille (cellule non vide = domaine singleton).
    2. Propage : toute cellule déjà fixée élimine sa valeur des autres cellules
       de la même ligne / colonne / bloc — élimination croisée entre pairs, la
       sémantique « N valeurs distinctes » du MDD de ligne (§4) sans en
       construire la structure (cf. note pédagogique §6.3).
    3. Backtracking sur la cellule au domaine minimal (heuristique MRV).
    Retourne True si la grille est résolue."""
    # Domaines : domaines[r][c] = set des valeurs possibles.
    domaines = [[set(range(1, size + 1)) for _ in range(size)] for _ in range(size)]
    for r in range(size):
        for c in range(size):
            if grid[r][c] != 0:
                domaines[r][c] = {grid[r][c]}

    def peers(r: int, c: int):
        """Cellules contraintes de ligne/colonne/bloc."""
        result = set()
        for k in range(size):
            if k != c:
                result.add((r, k))
            if k != r:
                result.add((k, c))
        br, bc = (r // 3) * 3, (c // 3) * 3
        for i in range(br, br + 3):
            for j in range(bc, bc + 3):
                if (i, j) != (r, c):
                    result.add((i, j))
        return result

    def propagate() -> bool:
        """Propagation : cellule fixée -> élimine sa valeur chez les peers.
        Retourne False si un domaine devient vide (échec)."""
        changed = True
        while changed:
            changed = False
            for r in range(size):
                for c in range(size):
                    if len(domaines[r][c]) == 1:
                        v = next(iter(domaines[r][c]))
                        for (pr, pc) in peers(r, c):
                            if v in domaines[pr][pc]:
                                domaines[pr][pc].discard(v)
                                changed = True
                                if len(domaines[pr][pc]) == 0:
                                    return False
        return True

    def select_mrv():
        """Sélectionne la cellule non fixée au domaine minimal (MRV)."""
        best = None
        best_size = size + 1
        for r in range(size):
            for c in range(size):
                d = domaines[r][c]
                if 1 < len(d) < best_size:
                    best_size = len(d)
                    best = (r, c)
        return best

    def backtrack() -> bool:
        if not propagate():
            return False
        cell = select_mrv()
        if cell is None:
            return True  # Toutes fixées -> résolu.
        r, c = cell
        snapshot = [[set(domaines[i][j]) for j in range(size)] for i in range(size)]
        for v in sorted(domaines[r][c]):
            # Restaurer le snapshot puis fixer (r,c) à v.
            for i in range(size):
                for j in range(size):
                    domaines[i][j] = set(snapshot[i][j])
            domaines[r][c] = {v}
            if backtrack():
                return True
        return False

    solved = backtrack()
    if solved:
        for r in range(size):
            for c in range(size):
                grid[r][c] = next(iter(domaines[r][c]))
    return solved


print("solve_sudoku_mdd défini (propagation de domaines + backtracking MRV).")

solve_sudoku_mdd défini (propagation de domaines + backtracking MRV).

6.3 Test du solveur

Résolvons une grille de Sudoku classique.

import time

# Grille de Sudoku classique (0 = case vide).
puzzle = [
    [5, 3, 0, 0, 7, 0, 0, 0, 0],
    [6, 0, 0, 1, 9, 5, 0, 0, 0],
    [0, 9, 8, 0, 0, 0, 0, 6, 0],
    [8, 0, 0, 0, 6, 0, 0, 0, 3],
    [4, 0, 0, 8, 0, 3, 0, 0, 1],
    [7, 0, 0, 0, 2, 0, 0, 0, 6],
    [0, 6, 0, 0, 0, 0, 2, 8, 0],
    [0, 0, 0, 4, 1, 9, 0, 0, 5],
    [0, 0, 0, 0, 8, 0, 0, 7, 9],
]

t0 = time.perf_counter()
solved = solve_sudoku_mdd(puzzle)
dt = time.perf_counter() - t0
print(f"Résolu en {dt*1000:.1f} ms : {solved}")
print("Grille solution :")
for row in puzzle:
    print(" ".join(str(v) for v in row))

Résolu en 1.4 ms : True
Grille solution :
5 3 4 6 7 8 9 1 2
6 7 2 1 9 5 3 4 8
1 9 8 3 4 2 5 6 7
8 5 9 7 6 1 4 2 3
4 2 6 8 5 3 7 9 1
7 1 3 9 2 4 8 5 6
9 6 1 5 3 7 2 8 4
2 8 7 4 1 9 6 3 5
3 4 5 2 8 6 1 7 9

Interprétation : solveur MDD

Le solveur combine deux idées :

1. Propagation de contraintes (style AC-3) : chaque cellule fixée élimine sa valeur chez ses peers (même ligne, colonne, bloc). C’est l’esprit du MDD comme filtre de domaines.
2. Backtracking avec heuristique MRV (Minimum Remaining Values) : on remplit d’abord la cellule la plus contrainte, ce qui réduit drastiquement le facteur de branchement.

Note pédagogique : la structure MDD complète (nœuds MDDNode) est utilisée ci-dessus (§4-5) pour représenter les contraintes ; le solveur pragmatique (§6) en extrait la sémantique (valeurs distinctes) pour une propagation efficace. Une implémentation complète propagerait directement sur la structure MDD (MDD-consistency), hors de portée de ce notebook d’introduction.

Exercice 3 : Comparer BDD et MDD sur des contraintes voisines

Le BDD et le MDD ne disent pas la même chose de la même façon. Comparez leurs tailles (count_nodes()) sur deux contraintes cousines, chacune dans son encodage naturel — les deux outils sont déjà dans le notebook :

• BDD (§2-3) : « exactement une variable vraie parmi N » sur N booléens — la fonction de l’Exercice 1, via exactly_one_of_n ;
• MDD (§4) : « N valeurs distinctes sur N cellules », une variable multi-valuée par cellule — via RowMDDBuilder.

Mesurez les deux, puis commentez le point que la comparaison illustre : le BDD est booléen — dès qu’une cellule Sudoku a 9 valeurs possibles, il faut 9 variables one-hot par cellule et la contrainte composée explose ; le MDD garde le domaine natif. La comparaison honnête n’est pas « la même contrainte » des deux côtés (l’encodage booléen complet de « tous différents » sur une ligne est précisément le blowup à démontrer) : c’est le prix de l’encodage pour exprimer la même information.

# EXERCICE : Comparer les performances BDD vs MDD
def compare_bdd_mdd():
    # TODO etudiant : construisez un BDD pour "exactement une variable vraie
    # parmi N" (N booléens) et un MDD pour "une cellule Sudoku ∈ {1..9} unique".
    # Etape 1 : construisez le BDD (N variables booléennes, via exactly_one_of_n).
    # Etape 2 : construisez le MDD (1 variable à 9 valeurs, via RowMDDBuilder).
    # Etape 3 : comparez count_nodes() et commentez la compacité.
    return None  # TODO etudiant


print("Exercice à compléter (comparaison BDD vs MDD).")

Exercice à compléter (comparaison BDD vs MDD).

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

7.1 Tableau comparatif

Critère	Sudoku-12 (Z3)	Sudoku-14 (BDD/MDD)
Approche	Solveur SMT générique	Structure de données explicite
Outil	Z3 (pyz3)	Hand-rolled (ce notebook)
Déclaratif ?	Oui (contraintes déclarées)	Non (construction explicite)
Pédagogique	Boîte noire	Internes visibles
Performance	Excellente (SAT solver CDCL)	Modeste (pas de réduction canonique)
Réutilisation	Toute contrainte exprimable	Spécialisé booléen/multi-valué

7.2 Quand utiliser quoi ?

• Z3 (Sudoku-12) : quand la contrainte est complexe, arithmétique, ou que la performance est critique. C’est l’outil SOTA pour la satisfiabilité.
• BDD/MDD (Sudoku-14) : quand on veut comprendre comment une fonction booléenne se factorise, ou qu’on a besoin de représenter canoniquement un ensemble de solutions (énumération, comptage).

Les deux sont complémentaires : Z3 est l’outil industriel, le BDD est l’outil pédagogique qui éclaire les internes de la résolution de contraintes.

Bilan

Ce notebook a présenté une implémentation hand-rolled des BDD et MDD en Python, jumeau pédagogique du notebook C#. Points clés retenus :

1. BDD = graphe acyclique représentant une fonction booléenne, avec réduction (deux enfants identiques → on remonte).
2. Apply = opération universelle (AND/OR/NOT via une seule fonction récursive mémoïsée sur la variable de tête).
3. MDD = généralisation multi-valuée, adaptée au Sudoku (cellules ∈ {1..9}).
4. Le solveur pragmatique combine propagation de domaines + backtracking MRV.

Parité : ce notebook Python est le jumeau de Sudoku-14-BDD-CSharp.ipynb. Les deux hand-rollent les mêmes structures (pas de lib BDD), pour enseigner les internes. Cf marathon parité (#4956).

Exercices supplémentaires

Exercice 4 : Inspection d’un BDD

Écrivez une fonction count_paths(bdd) qui compte le nombre de chemins menant à la feuille True (i.e. le nombre d’assignations satisfaisant la fonction).

Exercice 5 : Évaluation par lot

Étendez evaluate pour prendre une liste d’assignations et renvoyer la liste des résultats. Comparez le coût à une évaluation table-de-vérité naïve.

Références

• Bryant, R. E. (1986). Graph-Based Algorithms for Boolean Function Manipulation.
• dd — librairie BDD Python (pour aller plus loin).
• Notebook C# : Sudoku-14-BDD-CSharp.ipynb.
• Marathon parité : #4956.