O Cryptarithms é um jogo que consiste numa equação matemática entre números desconhecidos, cujos dígitos são representados por letras. Cada letra deve representar um dígito diferente e o dígito inicial de um número com vários dígitos não deve ser zero. Queremos saber os dígitos a que correspondem as letras envolvidas na seguinte equação:

$SEND + MORE = MONEY$

Podemos modelar o problema numa teoria de inteiros. Cada letra dá origem a uma variável inteira (𝑆,𝐸,𝑁,𝐷,𝑀,𝑂,𝑅 e 𝑌) e para representar a equação acima representamos cada parcela por uma expressão aritmética onde cada letra é multiplicada pelo seu “peso específico” em base 10.

Resolva o problema usando o Z3.

!pip install z3-solver

from z3 import *

S, E, N, D, M, O, R, Y = Ints('S E N D M O R Y')

s = Solver()

# >>> Restrições <<<
# Todas as variáveis são diferentes
s.add(Distinct(S, E, N, D, M, O, R, Y))
# S e M não podem ser 0
s.add(S > 0, M > 0)  # Nenhum dígito pode ser zero
# Tem que respeitar esta equiação : SEND + MORE = MONEY
s.add(S * 1000 + E * 100 + N * 10 + D + M * 1000 + O * 100 + R * 10 + E == M * 10000 + O * 1000 + N * 100 + E * 10 + Y)
# Cada variável tem que estar entre 0 e 9
for var in [S, E, N, D, M, O, R, Y]:
    s.add(And(0 <= var, var <= 9))

# Resolver
if s.check() == sat :
    m = s.model()
    # print(m) ==> [N = 6, E = 5, Y = 2, M = 1, S = 9, R = 8, O = 0, D = 7]
    for d in m.decls():
        print("%s = %d" % (d.name(), m[d].as_long()))
				 print("\\n")
else:
    print("Não tem solução.")

Para testar com mais soluções:

s.push()

# Contador de soluções
solution_count = 0

while s.check() == sat:
    solution_count += 1
    m = s.model()

    for d in m.decls():
        variable = d()
        value = m[d].as_long()
        print("%s = %d" % (d.name(), m[d].as_long()))

    print("\\n")
    s.add(Or([d() != m[d].as_long() for d in m.decls()]))

print("Total de soluções encontradas: %d" % solution_count)

s.pop()