Alphametics and Z3 SMT solver

According to Donald Knuth, the term "Alphametics" was coined by J. A. H. Hunter. This is a puzzle: what decimal digits in 0..9 range must be assigned to each letter, so the following equation will be true?

  SEND
+ MORE
 -----
 MONEY

This is easy for Z3:

from z3 import *

# SEND+MORE=MONEY

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

s=Solver()

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

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)

print s.check()
print s.model()


Output:

sat
[E, = 5,
 S, = 9,
 M, = 1,
 N, = 6,
 D, = 7,
 R, = 8,
 O, = 0,
 Y = 2]

Another one, also from TAOCP volume IV (http://www-cs-faculty.stanford.edu/~uno/fasc2b.ps.gz):

from z3 import *

# VIOLIN+VIOLIN+VIOLA = TRIO+SONATA

A, I, L, N, O, R, S, T, V = Ints('A, I, L, N, O, R, S, T, V')

s=Solver()

s.add(Distinct(A, I, L, N, O, R, S, T, V))
s.add(And(A>=0, A<=9))
s.add(And(I>=0, I<=9))
s.add(And(L>=0, L<=9))
s.add(And(N>=0, N<=9))
s.add(And(O>=0, O<=9))
s.add(And(R>=0, R<=9))
s.add(And(S>=0, S<=9))
s.add(And(T>=0, T<=9))
s.add(And(V>=0, V<=9))

VIOLIN, VIOLA, SONATA, TRIO = Ints('VIOLIN, VIOLA, SONATA, TRIO')

s.add(VIOLIN==100000*V+10000*I+1000*O+100*L+10*I+N)
s.add(VIOLA==10000*V+1000*I+100*O+10*L+A)
s.add(SONATA==100000*S+10000*O+1000*N+100*A+10*T+A)
s.add(TRIO==1000*T+100*R+10*I+O)

s.add(VIOLIN+VIOLIN+VIOLA == TRIO+SONATA)

print s.check()
print s.model()


sat
[L, = 6,
 S, = 7,
 N, = 2,
 T, = 1,
 I, = 5,
 V = 3,
 A, = 8,
 R, = 9,
 O, = 4,
 TRIO = 1954,
 SONATA, = 742818,
 VIOLA, = 35468,
 VIOLIN, = 354652]

This puzzle I've found in pySMT examples:

from z3 import *

# H+E+L+L+O = W+O+R+L+D = 25

H, E, L, O, W, R, D = Ints ('H, E, L, O, W, R, D')

s=Solver()

s.add(Distinct(H, E, L, O, W, R, D))
s.add(And(H>=1, H<=9))
s.add(And(E>=1, E<=9))
s.add(And(L>=1, L<=9))
s.add(And(O>=1, O<=9))
s.add(And(W>=1, W<=9))
s.add(And(R>=1, R<=9))
s.add(And(D>=1, D<=9))

s.add(H+E+L+L+O == W+O+R+L+D == 25)

print s.check()
print s.model()


sat
[E, = 4, D = 6, O, = 2, W, = 3, R, = 5, L, = 1, H, = 9]

This is exercise Q209 from the "Companion to the Papers of Donald Knuth":

 KNIFE
  FORK
 SPOON
  SOUP
------
SUPPER

I've added a helper function (list_to_expr()) to make things simpler:

from z3 import *

# KNIFE+FORK+SPOON+SOUP = SUPPER

E, F, I, K, N, O, P, R, S, U = Ints('E F I K N O P R S U')

s=Solver()

s.add(Distinct(E, F, I, K, N, O, P, R, S, U))
s.add(And(E>=0, E<=9))
s.add(And(F>=0, F<=9))
s.add(And(I>=0, I<=9))
s.add(And(K>=0, K<=9))
s.add(And(N>=0, N<=9))
s.add(And(O>=0, O<=9))
s.add(And(P>=0, P<=9))
s.add(And(R>=0, R<=9))
s.add(And(S>=0, S<=9))
s.add(And(U>=0, U<=9))

#s.add(S!=0)

KNIFE, FORK, SPOON, SOUP, SUPPER = Ints('KNIFE FORK SPOON SOUP SUPPER')

# construct expression in form like:
# 10000000*L+1000000*U+100000*N+10000*C+1000*H+100*E+10*O+N
def list_to_expr(lst):
    coeff=1
    _sum=0
    for var in lst[::-1]:
        _sum=_sum+var*coeff
        coeff=coeff*10
    return _sum

s.add(KNIFE==list_to_expr([K,N,I,F,E]))
s.add(FORK==list_to_expr([F,O,R,K]))
s.add(SPOON==list_to_expr([S,P,O,O,N]))
s.add(SOUP==list_to_expr([S,O,U,P]))
s.add(SUPPER==list_to_expr([S,U,P,P,E,R]))

s.add(KNIFE+FORK+SPOON+SOUP == SUPPER)

print s.check()
print s.model()


sat
[K = 7,
 N = 4,
 R = 9,
 I = 1,
 E = 6,
 S = 0,
 O = 3,
 F = 5,
 U = 8,
 P = 2,
 SUPPER = 82269,
 SOUP = 382,
 SPOON = 2334,
 FORK = 5397,
 KNIFE = 74156]

S is zero, so SUPPER value is starting with leading (removed) zero. Let's say, we don't like it. Add this to resolve it:

s.add(S!=0)
sat
[K = 8,
 N = 4,
 R = 3,
 I = 7,
 E = 6,
 S = 1,
 O = 9,
 F = 2,
 U = 0,
 P = 5,
 SUPPER = 105563,
 SOUP = 1905,
 SPOON = 15994,
 FORK = 2938,
 KNIFE = 84726]

Devising your own puzzle

Here is a problem: you can only use 10 letters, but how to select them among words? We can try to offload this task to Z3:

from z3 import *

def char_to_idx(c):
    return ord(c)-ord('A')

def idx_to_char(i):
    return chr(ord('A')+i)

# construct expression in form like:
# 10000000*L+1000000*U+100000*N+10000*C+1000*H+100*E+10*O+N
def list_to_expr(lst):
    coeff=1
    _sum=0
    for var in lst[::-1]:
        _sum=_sum+var*coeff
        coeff=coeff*10
    return _sum

# this table has 10 items, it reflects character for each number:
digits=[Int('digit_%d' % i) for i in range(10)]

# this is "reverse" table, it has value for each letter:
letters=[Int('letter_%d' % i) for i in range(26)]

s=Solver()

# all items in digits[] table must be distinct, because no two letters can share same number:
s.add(Distinct(digits))

# all numbers are in 0..25 range, because each number in this table defines character:
for i in range(10):
    s.add(And(digits[i]>=0,digits[i]<26))

# define "reverse" table.
# letters[i] is 0..9, depending on which digits[] item contains this letter:
for i in range(26):
    s.add(letters[i] == 
        If(digits[0]==i,0,
        If(digits[1]==i,1,
        If(digits[2]==i,2,
        If(digits[3]==i,3,
        If(digits[4]==i,4,
        If(digits[5]==i,5,
        If(digits[6]==i,6,
        If(digits[7]==i,7,
        If(digits[8]==i,8,
        If(digits[9]==i,9,99999999)))))))))))

# the last word is "sum" all the rest are "addends":

words=['APPLE', 'BANANA', 'BREAD', 'CAKE', 'CAVIAR', 'CHEESE', 'CHIPS', 'COFFEE', 'EGGS', 'FISH', 'HONEY', 'JAM', 'JELLY', 'JUICE', 'MILK', 'OATMEAL', 'ORANGE', 'PANCAKE', 'PIZZA', 'STEAK', 'TEA', 'TOMATO', 'WAFFLE', 'LUNCH']

words_total=len(words)

word=[Int('word_%d' % i) for i in range(words_total)]
word_used=[Bool('word_used_%d' % i) for i in range(words_total)]

# last word is always used:
s.add(word_used[words_total-1]==True)

#s.add(word_used[words.index('CAKE')])
s.add(word_used[words.index('EGGS')])

for i in range(words_total):
    # get list of letters for the word:
    lst=[letters[char_to_idx(c)] for c in words[i]]
    # construct expression for letters. it must be equal to the value of the word:
    s.add(word[i]==list_to_expr(lst))
    # if word_used, word's value must be less than 99999999, i.e., all letters are used in the word:
    s.add(If(word_used[i], word[i], 0) < 99999999)

# if word_used, add value of word to the whole expression
expr=[If(word_used[i], word[i], 0) for i in range(words_total-1)]
# sum up all items in expression. sum must be equal to the value of the last word:
s.add(sum(expr)==word[-1])

print s.check()
m=s.model()
#print m

for i in range(words_total):
    # if word_used, print it:
    if str(m[word_used[i]])=="True" or i+1==words_total:
        print words[i]

for i in range(26):
    # it letter is used, print it:
    if m[letters[i]].as_long()!=99999999:
        print idx_to_char(i), m[letters[i]]


This is the first generated puzzle:

sat
EGGS
JELLY
LUNCH
C 5
E 6
G 3
H 7
J 0
L 1
N 4
S 8
U 2
Y 9

What if we want to "CAKE" be present among "addends"?

Add this:

s.add(word_used[words.index('CAKE')])
sat
CAKE
TEA
LUNCH
A 8
C 3
E 1
H 9
J 6
K 2
L 0
N 5
T 7
U 4

Add this:

s.add(word_used[words.index('EGGS')])

Now it can find pair to EGGS:

sat
EGGS
HONEY
LUNCH
C 6
E 7
G 9
H 4
L 5
N 8
O 2
S 3
U 0
Y 1

The files

https://github.com/dennis714/yurichev.com/tree/master/blog/alphametics

→ [list of blog posts, my twitter/facebook]

Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.