Solving a Cryptarithmetic puzzle using Z3

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(Or(self.X[i]==2, self.X[i]==3, self.X[i]==5, self.X[i]==7))  
        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])) 
        self.s.add(self.X[8]==self.X[13])

    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