That Was Easy

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:

[python]
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])

[/python]

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.

1 thought on “That Was Easy”

  1. Cool example! Yes, the SMT-LIB standard (and the Python API) provides a distinct term that allows you to reduce the uniqueness constraint to the following:

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

    Here’s also proof of equivalence in the online rise4fun interface: http://rise4fun.com/Z3Py/3CI

Comments are closed.