← 09 - Enigme d’Einstein | README Z3-Python # 10. Cryptarithmes (SEND + MORE = MONEY) Un cryptarithme est une equation arithmetique ou chaque lettre represente un chiffre distinct (0-9), et ou les mots formant l’equation correspondent a des nombres en ecriture positionnelle. Le classique SEND + MORE = MONEY admet une unique solution : laquelle ? Ce type de puzzle est un cas canonique de satisfaction de contraintes sur les entiers : 8 lettres, chacune dans {0..9}, deux a deux distinctes, avec des tetes non nulles (S et M) et une equation lineaire positionnelle. La propagation de contraintes du solveur SMT resout instantanement ce que la brute force met plusieurs centaines de millisecondes a enumerer. > Port pyz3 du notebook C# 13_Cryptarithmetic_SMT.ipynb (Microsoft.Z3 brut). EPIC #1206, Prong B.

from z3 import *
import time
print("Imports OK : z3-solver (pyz3)")
Imports OK : z3-solver (pyz3)

Modelisation : SEND + MORE = MONEY

On encode chaque lettre comme un entier Int dans {0..9}, on impose la distinction globale (Distinct), les têtes non nulles (S > 0, M > 0), puis l’equation positionnelle :

  1000*S + 100*E + 10*N + D     (SEND)
+ 1000*M + 100*O + 10*R + E     (MORE)
= 10000*M + 1000*O + 100*N + 10*E + Y   (MONEY)

Z3 propage ces contraintes et renvoie l’unique modèle.

# Cryptarithme classique : SEND + MORE = MONEY
s = Solver()
S, E, N, D, M, O, R, Y = Ints('S E N D M O R Y')
letters = [S, E, N, D, M, O, R, Y]

# (1) Domaine 0..9 pour chaque lettre
s.add([And(v >= 0, v <= 9) for v in letters])

# (2) Les 8 lettres sont deux a deux distinctes (contrainte globale)
s.add(Distinct(letters))

# (3) Tetes non nulles (pas de zero non-significatif)
s.add(S > 0, M > 0)

# (4) Equation arithmetique positionnelle : SEND + MORE == MONEY
s.add((1000*S + 100*E + 10*N + D) +
      (1000*M + 100*O + 10*R + E) ==
      (10000*M + 1000*O + 100*N + 10*E + Y))

if s.check() != sat:
    print("UNSAT : aucune solution (inattendu pour ce cryptarithme)")
else:
    m = s.model()
    send  = 1000*m[S].as_long() + 100*m[E].as_long() + 10*m[N].as_long() + m[D].as_long()
    more  = 1000*m[M].as_long() + 100*m[O].as_long() + 10*m[R].as_long() + m[E].as_long()
    money = 10000*m[M].as_long() + 1000*m[O].as_long() + 100*m[N].as_long() + 10*m[E].as_long() + m[Y].as_long()
    print("  S=%d E=%d N=%d D=%d  M=%d O=%d R=%d Y=%d" % (m[S].as_long(), m[E].as_long(), m[N].as_long(), m[D].as_long(),
                                                            m[M].as_long(), m[O].as_long(), m[R].as_long(), m[Y].as_long()))
    print("    %5d" % send)
    print("  + %5d" % more)
    print("  -------")
    print("  %5d    (%d + %d = %d, verifie = %s)" % (money, send, more, money, send + more == money))
  S=9 E=5 N=6 D=7  M=1 O=0 R=8 Y=2
     9567
  +  1085
  -------
  10652    (9567 + 1085 = 10652, verifie = True)

Interpretation

La solution unique est S=9 E=5 N=6 D=7 M=1 O=0 R=8 Y=2, soit 9567 + 1085 = 10652. Notez le rôle de la retenue : ce n’est pas evident a l’oeil, c’est la propagation arithmetique du solveur qui la deduit automatiquement a partir de l’equation positionnelle. Aucune boucle explicite sur les retenues n’est necessaire : c’est précisément ce que Z3 fait mieux qu’un code imperatif.

Anatomie : où sont passées les retenues ?

L’encodage ci-dessus n’introduit aucune variable de retenue — et pourtant l’addition posée à la main en exige. Reconstituons la chaîne des retenues que la propagation de Z3 retrouve implicitement, en notant \(c_i\) la retenue sortant de la colonne \(i\) (de droite à gauche) :

Colonne Équation manuelle Avec la solution mesurée
unités \(D + E = 10 c_1 + Y\) \(7 + 5 = 12\), donc \(c_1 = 1\), \(Y = 2\)
dizaines \(N + R + c_1 = 10 c_2 + E\) \(6 + 8 + 1 = 15\), donc \(c_2 = 1\), \(E = 5\)
centaines \(E + O + c_2 = 10 c_3 + N\) \(5 + 0 + 1 = 6\), donc \(c_3 = 0\), \(N = 6\)
milliers \(S + M + c_3 = 10 c_4 + O\) \(9 + 1 + 0 = 10\), donc \(c_4 = 1\), \(O = 0\)
dizaines de milliers \(c_4 = M\) \(1 = M\)

Toute cette chaîne est subsumée par l’unique équation linéaire positionnelle : l’arithmétique entière de Z3 raisonne sur l’égalité \(9567 + 1085 = 10652\) comme sur n’importe quelle identité entière, sans qu’on ait à décomposer les colonnes. Le chiffre de tête \(M = 1\) n’est rien d’autre que la dernière retenue devenue chiffre significatif — le solveur la déduit, il ne la déclare pas.

Approche naive vs solveur : que fait la propagation ?

La brute force enumere tous les arrangements P(10, 8) = 10!/(10-8)! = 1 814 400 candidats (8 lettres distinctes prises parmi 10 chiffres), puis teste l’equation pour chacun. Le solveur, lui, propage les contraintes (distinction, domaines, equation) pour eliminer en bloc des familles entieres d’affectations impossibles avant même de les tester. Mesurons l’ecart.

# (1) Brute force : 8 boucles imbriquees, on saute des que deux lettres coincident
#     P(10,8) = 1 814 400 candidats distincts testes.
nb_brute = 0
t0 = time.perf_counter()
for S in range(10):
 for E in range(10):
  if E == S: continue
  for N in range(10):
   if N in (S, E): continue
   for D in range(10):
    if D in (S, E, N): continue
    for M in range(10):
     if M in (S, E, N, D): continue
     for O in range(10):
      if O in (S, E, N, D, M): continue
      for R in range(10):
       if R in (S, E, N, D, M, O): continue
       for Y in range(10):
        if Y in (S, E, N, D, M, O, R): continue
        if S > 0 and M > 0:
            send  = 1000*S + 100*E + 10*N + D
            more  = 1000*M + 100*O + 10*R + E
            money = 10000*M + 1000*O + 100*N + 10*E + Y
            if send + more == money:
                nb_brute += 1
t_brute = time.perf_counter() - t0

# (2) Z3 : meme theoreme que la cellule precedente, mesure
t0 = time.perf_counter()
nb_z3 = 0
s2 = Solver()
S2, E2, N2, D2, M2, O2, R2, Y2 = Ints('S2 E2 N2 D2 M2 O2 R2 Y2')
L2 = [S2, E2, N2, D2, M2, O2, R2, Y2]
s2.add([And(v >= 0, v <= 9) for v in L2])
s2.add(Distinct(L2))
s2.add(S2 > 0, M2 > 0)
s2.add((1000*S2 + 100*E2 + 10*N2 + D2) + (1000*M2 + 100*O2 + 10*R2 + E2) ==
       (10000*M2 + 1000*O2 + 100*N2 + 10*E2 + Y2))
if s2.check() == sat:
    nb_z3 = 1
t_z3 = time.perf_counter() - t0

print("Brute force : %d solution(s) en %.1f ms  (1 814 400 candidats testes)" % (nb_brute, t_brute * 1000))
print("Z3 solve    : %d solution(s) en %.1f ms  (propagation de contraintes)" % (nb_z3, t_z3 * 1000))
print(" -> meme resultat (%s), strategies differentes." % (nb_brute == nb_z3))
Brute force : 1 solution(s) en 9409.2 ms  (1 814 400 candidats testes)
Z3 solve    : 1 solution(s) en 58.6 ms  (propagation de contraintes)
 -> meme resultat (True), strategies differentes.

Lecture du benchmark

L’ecart est net : la brute force teste 1 814 400 affectations pour trouver l’unique solution, tandis que Z3 la trouve en quelques millisecondes via propagation. Ce n’est pas une question de vitesse brute du langage : c’est la nature de la recherche. Le solveur ne << teste >> pas, il deduit - les contraintes Distinct et l’equation positionnelle reduisent l’espace avant tout branchement. C’est l’intérêt pedagogique central : sur un problème combinatoire, declarer les contraintes bat l’enumeration imperative.

Témoin et preuve : deux niveaux de garantie

check() renvoie sat et un modèle : c’est un témoignage — la preuve qu’il existe au moins une solution. Il ne dit rien de leur nombre. Le texte ci-dessus affirme que SEND + MORE = MONEY admet une solution unique : cette affirmation ne tombe pas du modèle, elle se prouve en re-posant la question à Z3 (bloquer la solution trouvée, puis vérifier l’insatisfiabilité — exactement l’objet de l’exercice 2). Distinguer témoin (existence) et preuve d’exhaustivité (unicité) est le réflexe central que ces notebooks cherchent à installer.

Variante : CROSS + ROADS = DANGER (9 lettres distinctes)

On complique : 9 lettres distinctes (C, R, O, S, A, D, N, G, E), trois têtes non nulles (C, R, D), et une equation a 6 chiffres en résultats. La brute force devrait enumerer P(10, 9) = 3 628 800 candidats - le solveur reste instantane.

# Variante : CROSS + ROADS = DANGER (9 lettres distinctes)
s3 = Solver()
C, R, O, S, A, D, N, G, E = Ints('C R O S A D N G E')
L3 = [C, R, O, S, A, D, N, G, E]

# Domaine 0..9 pour les 9 lettres
s3.add([And(v >= 0, v <= 9) for v in L3])

# 9 lettres deux a deux distinctes
s3.add(Distinct(L3))

# Tetes non nulles : C (CROSS), R (ROADS), D (DANGER)
s3.add(C > 0, R > 0, D > 0)

# CROSS + ROADS == DANGER
# CROSS  = 10000*C + 1000*R + 100*O + 10*S + S
# ROADS  = 10000*R + 1000*O + 100*A + 10*D + S
# DANGER = 100000*D + 10000*A + 1000*N + 100*G + 10*E + R
s3.add((10000*C + 1000*R + 100*O + 10*S + S) +
       (10000*R + 1000*O + 100*A + 10*D + S) ==
       (100000*D + 10000*A + 1000*N + 100*G + 10*E + R))

if s3.check() != sat:
    print("UNSAT : aucune solution pour CROSS + ROADS = DANGER")
else:
    m = s3.model()
    cross  = 10000*m[C].as_long() + 1000*m[R].as_long() + 100*m[O].as_long() + 10*m[S].as_long() + m[S].as_long()
    roads  = 10000*m[R].as_long() + 1000*m[O].as_long() + 100*m[A].as_long() + 10*m[D].as_long() + m[S].as_long()
    danger = 100000*m[D].as_long() + 10000*m[A].as_long() + 1000*m[N].as_long() + 100*m[G].as_long() + 10*m[E].as_long() + m[R].as_long()
    print("CROSS=%d  ROADS=%d  DANGER=%d   (%d + %d = %d, egal a DANGER = %d : %s)" %
          (cross, roads, danger, cross, roads, cross + roads, danger, cross + roads == danger))
CROSS=96233  ROADS=62513  DANGER=158746   (96233 + 62513 = 158746, egal a DANGER = 158746 : True)

Lecture de la variante CROSS + ROADS = DANGER

La solution mesurée est CROSS = 96233, ROADS = 62513, DANGER = 158746. Trois observations structurelles :

  1. D = 1 est forcé avant toute recherche : la somme de deux nombres à 5 chiffres reste inférieure à 200 000, et le résultat à 6 chiffres impose D différent de 0 — donc D = 1. Là encore, la retenue finale devient le chiffre de tête du résultat.
  2. La lettre S travaille trois fois : elle occupe les dizaines et les unités de CROSS, plus les unités de ROADS. Cette réutilisation croise les colonnes entre elles — pour une résolution manuelle, c’est une complication ; pour l’équation linéaire, ce n’est qu’un coefficient répété.
  3. Un seul chiffre reste absent : les neuf lettres reçoivent 9, 6, 2, 3, 5, 1, 0, 8, 7 — il manque le 4. Avec 9 lettres distinctes prises parmi 10 chiffres, l’affectation est proche d’une permutation complète : l’espace brut double (\(P(10,9) = 3\,628\,800\) contre \(1\,814\,400\)). Le notebook ne mesure pas le temps du solveur sur cette variante — un prolongement naturel, conjointement à la question de l’unicité (exercice 2).

Exercices

Les trois exercices ci-dessous vous font manipuler l’encodage des cryptarithmes (domaine, distinction, equation positionnelle) sur des variantes classiques. Ils progressent du modelisation d’une nouvelle equation (1), a l’enumeration complete des solutions (2), puis a la generalisation a la multiplication (3). Chaque stub est self-contained : les fonctions utilitaires (Solver, Ints, Distinct) sont définies dans les sections précédentes.

Exercice 1 - DONALD + GERALD = ROBERT

Modelisez le cryptarithme DONALD + GERALD = ROBERT (10 lettres distinctes : D, O, N, A, L, G, E, R, B, T).

Étapes : 1. Variables Ints pour les 10 lettres, domaine {0..9}. 2. Distinct sur les 10 lettres. 3. Tetes non nulles : D > 0, G > 0, R > 0. 4. Equation positionnelle : - DONALD = 100000*D + 10000*O + 1000*N + 100*A + 10*L + L - GERALD = 100000*G + 10000*E + 1000*R + 100*A + 10*L + D - ROBERT = 100000*R + 10000*O + 1000*B + 100*E + 10*R + T

Indice : notez que L apparait deux fois dans DONALD (unite et dizaine) et R deux fois dans ROBERT - le solveur s’en occupe, il suffit d’ecrire l’equation positionnelle correcte.

# Exercice 1 : DONALD + GERALD = ROBERT
# TODO etudiant :
# Etape 1 : D, O, N, A, L, G, E, R, B, T = Ints('D O N A L G E R B T')
# Etape 2 : domaine 0..9 pour les 10 lettres
# Etape 3 : Distinct(...) sur les 10 lettres
# Etape 4 : têtes non nulles (D > 0, G > 0, R > 0)
# Etape 5 : equation DONALD + GERALD == ROBERT
result = None  # TODO etudiant
print("Exercice 1 a completer : modelisez DONALD + GERALD = ROBERT avec Z3")
Exercice 1 a completer : modelisez DONALD + GERALD = ROBERT avec Z3

Exercice 2 - Verifier l’unicite de la solution

Combien de solutions admet SEND + MORE = MONEY ? On sait qu’il y en a au moins une (cellule 3). Pour prouver l’unicite, on ajoute une contrainte qui nie la solution trouvee et on re-teste : si unsat, la solution etait unique.

Étapes : 1. Re-resoudre SEND + MORE = MONEY, recupere le modèle m. 2. Ajouter la contrainte de negation : Or(S != m[S], E != m[E], ...) (au moins une lettre differe). 3. Re-checker : si unsat -> unique ; si sat -> il existe une autre solution (compter par itération).

# Exercice 2 : prouver l'unicite de SEND + MORE = MONEY
# TODO etudiant :
# 1. Re-resoudre, recuperer le modele m
# 2. Ajouter Or(S != m[S], E != m[E], N != m[N], ...) pour nier la solution
# 3. Si unsat -> unique ; sinon compter toutes les solutions par iteration
nb_solutions = None  # TODO etudiant
print("Exercice 2 a completer : prouvez l'unicite (ou enumerez toutes les solutions)")
Exercice 2 a completer : prouvez l'unicite (ou enumerez toutes les solutions)

Exercice 3 - Cryptarithme avec produit (multiplication)

Generalisez a la multiplication : ABC * D = DBC, ou ABC = 100*A + 10*B + C et DBC = 100*D + 10*B + C.

Étapes : 1. Variables A, B, C, D = Ints('A B C D'), domaine {0..9}. 2. Distinct(A, B, C, D), têtes A > 0 et D > 0. 3. Equation : (100*A + 10*B + C) * D == (100*D + 10*B + C).

Indice : c’est la même structure que l’addition, mais l’opérateur * remplace +. Z3 traite les deux aussi bien (théorie arithmetique lineaire + non-lineaire).

# Exercice 3 : ABC * D = DBC (multiplication)
# TODO etudiant :
# 1. A, B, C, D = Ints('A B C D'), domaine 0..9
# 2. Distinct(A, B, C, D), têtes A > 0 et D > 0
# 3. Equation : (100*A + 10*B + C) * D == (100*D + 10*B + C)
result = None  # TODO etudiant
print("Exercice 3 a completer : modelisez ABC * D = DBC")
Exercice 3 a completer : modelisez ABC * D = DBC

Conclusion

Les cryptarithmes illustrent un avantage central du paradigme declaretif : on exprime ce qu’on cherche (une affectation de chiffres distincts satisfaisant une equation positionnelle), pas comment le chercher. Le solveur Z3 se charge de la recherche via propagation de contraintes - instantanement la ou la brute force enumere des millions de candidats.

Cette serie Z3-Python (notebooks 01 a 10) couvre maintenant le spectre complet : satisfaction de contraintes (01, 02), tactiques (03), chaînes/regex (04), quantificateurs (05), optimisation avancee (06), style declaratif (07), ordonnancement NP-difficile (08), CSP logique (09), et ici l’arithmetique symbolique sur entiers (10). Le pont avec la serie sœur Z3.Linq (C#) se fait via les mêmes exemples portes entre Microsoft.Z3 et pyz3.

Retour au sommet