I wanted to play around with the Python interface to Z3 and the classic SEND + MORE = MONEY puzzle seemed like a good way to get started. This turned out to be so easy that my code worked almost on the first try:

from z3 import *

# find the (distinct) integer value in 0..9 for each letter that makes
# this equation work:
#
#   SEND
# + MORE
# ------
#  MONEY

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

s = Solver()

s.add (S >= 0, S < 10, 
       E >= 0, E < 10, 
       N >= 0, N < 10, 
       D >= 0, D < 10, 
       M >= 0, M < 10, 
       O >= 0, O < 10, 
       R >= 0, R < 10, 
       Y >= 0, Y < 10)

s.add ((D + 10*N + 100*E + 1000*S + 
        E + 10*R + 100*O + 1000*M) == 
       (Y + 10*E + 100*N + 1000*O + 10000*M))

s.add (S != E, S != N, S != D, S != M, S != O, S != R, S != Y, 
       E != N, E != D, E != M, E != O, E != R, E != Y, 
       N != D, N != M, N != O, N != R, N != Y, 
       D != M, D != O, D != R, D != Y, 
       M != O, M != R, M != Y, 
       O != R, O != Y, 
       R != Y)

print s.check()
m = s.model()
for d in m.decls():
    print "%s = %s" % (d.name(), m[d])

Then:

$ python ./send_more_money.py
sat
D = 7
S = 9
N = 6
O = 0
R = 8
E = 5
M = 1
Y = 2

Is there a non-quadratic way to express the uniqueness constraint? That would be nice. Anyhow, it’s really a pleasure when research software is this easy to use.

UPDATE: There is a better way! See comment #1 below. Thanks Taylor.