# Solving a Cryptarithmetic puzzle using Z3

Using the fantastic Z3 for fun.

Published

December 3, 2019

## Puzzle

Replace “P” with a prime integer below to ensure that the multiplication is valid

``````    P P P
x P P
---------
P P P P
P P P P
---------
P P P P P``````

## Python code using Z3

``````from z3 import *

class CASolver:
def __init__(self):
self.X = [Int("x_%s" % j) for j in range(18)]
self.s = Solver()
for i in range(0,18):
self.s.add(((100*self.X[2]+10*self.X[1]+self.X[0])*self.X[3]) == (1000*self.X[5] + 100*self.X[6] + 10*self.X[7] + self.X[8]))
self.s.add(((100*self.X[2]+10*self.X[1]+self.X[0])*self.X[4]) == (1000*self.X[9] + 100*self.X[10] + 10*self.X[11] + self.X[12]))
self.s.add((100*self.X[5]+10*self.X[6]+self.X[7] + 1000*self.X[9]+100*self.X[10]+10*self.X[11] + self.X[12]) == (1000*self.X[17]+100*self.X[16]+10*self.X[15]+self.X[14]))

def solve(self):
if self.s.check() == sat:
self.output_solution()

def output_solution(self):
m = self.s.model()
print(str(m.evaluate(self.X[2])), str(m.evaluate(self.X[1])), str(m.evaluate(self.X[0])))
print(str(m.evaluate(self.X[4])), str(m.evaluate(self.X[3])))
print(str(m.evaluate(self.X[5])), str(m.evaluate(self.X[6])), str(m.evaluate(self.X[7])), str(m.evaluate(self.X[8])))
print(str(m.evaluate(self.X[9])), str(m.evaluate(self.X[10])), str(m.evaluate(self.X[11])), str(m.evaluate(self.X[12])))
print(str(m.evaluate(self.X[17])), str(m.evaluate(self.X[16])), str(m.evaluate(self.X[15])), str(m.evaluate(self.X[14])), str(m.evaluate(self.X[13])))

s = CASolver()
s.solve()``````

## Solution

``````    7 7 5
x 3 3
---------
2 3 2 5
2 3 2 5
---------
2 5 5 7 5``````