# Solving Kakuro using Z3

Using the fantastic Z3 for fun.
Z3
puzzles
Published

March 2, 2020

## Kakuro

Kakuro is like a crossword puzzle with numbers. Each “word” must add up to the number provided in the clue above it or to the left. Words can only use the numbers 1 through 9, and a given number can only be used once in a word.

Here is a hard Kakuro puzzle

## Solution using Z3

Here is how the above puzzle is encoded:

``````x,38|,29|,x,10|,14|,x,21|,16|,14|
|14,_,_,|6,_,_,|16,_,_,_
|16,_,_,5|13,_,_,13|23,_,_,_
|26,_,_,_,_,12|16,_,_,33|,31|
|10,_,_,_,21|15,_,_,_,_,_
|6,_,_,14|22,_,_,_,9|15,_,_
|16,_,_,_,_,_,12|7,_,_,_
x,17|,5|9,_,_,8|30,_,_,_,_
|11,_,_,_,|3,_,_,|17,_,_
|19,_,_,_,|9,_,_,|3,_,_``````

Here is the python code using Z3

``````import sys
from z3 import *

class KakuroSolver:
def __init__(self, fp):
self.rows = len(self.inp)
self.cols = len(self.inp[0])
self.X_map = {(i, j): Int("x_%s_%s" % (i+1, j+1)) for (i, j) in self.vars}
self.s = Solver()
self.s.add([And(1 <= v, v <= 9) for v in self.X_map.values()])

X = []
with(open(fp, "r")) as f:
X.append(line.strip("\n").split(","))
var_pos = [(i, j) for (i, l) in enumerate(X) for (j, t) in enumerate(l) if t == "_"]
return X, var_pos

def set_constraints(self):
for i in range(self.rows):
for j in range(self.cols):
if "|" in self.inp[i][j]:
c, r = self.inp[i][j].split("|")
if r:
bvars, r_p = [], j+1
while (r_p < self.cols  and self.inp[i][r_p] == "_"):
bvars.append(self.X_map[(i, r_p)])
r_p += 1
if c:
bvars, c_p = [], i+1
while (c_p <self.rows and self.inp[c_p][j] == "_"):
bvars.append(self.X_map[(c_p, j)])
c_p += 1

def print_grid(self):
print("Here is the solution")
m = self.s.model()
for i in range(self.rows):
print("  ".join(['{:>3}'.format(str(m.eval(self.X_map[(i, j)]))) if self.inp[i][j] == "_" else '{:>3}'.format(" ")
for j in range(self.cols)]))

def solve(self):
self.set_constraints()
if self.s.check() == sat:
self.print_grid()
else:
print("Failed to solve the puzzle")

if __name__ == "__main__":
ks = KakuroSolver(sys.argv[1])
ks.solve()``````