# Solving Kakurasu using Z3

#### Using the fantastic Z3 for fun.

By Vamshi Jandhyala in Z3 python

October 29, 2019

## Kakurasu

Kakurasu is played on a rectangular grid with no standard size. The goal is to make some of the cells black in such a way that:

- The black cells on each row sum up to the number on the right.
- The black cells on each column sum up to the number on the bottom.
- If a black cell is first on its row/column its value is 1. If it is second its value is 2 etc.

Here is a $9\times9$ hard Kakurasu puzzle

## Python code using Z3

```
from z3 import *
import seaborn as sns
sns.set()
class KakurasuSolver:
def __init__(self, n, puzzle, outputfilename):
self.n = n
self.input = puzzle
self.output = outputfilename
self.X = [[Int("x_%s_%s" % (i+1, j+1)) for j in range(n)]
for i in range(n)]
self.s = Solver()
self.s.add([And(0 <= self.X[i][j], self.X[i][j]<= 1) for i in range(n) for j in range(n)])
def set_constraints(self):
for d, n, s in self.input:
if d == "C":
self.s.add(And(sum([(i+1)*self.X[i][n-1] for i in range(0,self.n)]) == s))
if d == "R":
self.s.add(And(sum([(i+1)*self.X[n-1][i] for i in range(0,self.n)]) == s))
def output_solution(self):
m = self.s.model()
data = [[int(str(m.evaluate(self.X[i][j])))*-1 for j in range(self.n)] for i in range(self.n)]
snsplot = sns.heatmap(data, square=True, linewidths=1.0, xticklabels=False, yticklabels=False, cbar=False)
snsplot.get_figure().savefig(self.outputfilename + ".png")
def solve(self):
self.set_constraints()
if self.s.check() == sat:
self.output_solution()
else:
print(self.s)
print("Failed to solve.")
puzzle = [
("C",1,18),
("C",2,4),
("C",3,14),
("C",4,23),
("C",5,8),
("C",6,20),
("C",7,24),
("C",8,39),
("C",9,33),
("R",1,8),
("R",2,27),
("R",3,23),
("R",4,33),
("R",5,34),
("R",6,1),
("R",7,28),
("R",8,24),
("R",9,30),
]
outputfilename = "kakurasu_sol"
ks = KakurasuSolver(9, puzzle, outputfilename)
ks.solve()
```

## Solution

The solution for above puzzle is given below