Solving Kakurasu using Z3

Using the fantastic Z3 for fun.

October 29, 2019


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:

  1. The black cells on each row sum up to the number on the right.
  2. The black cells on each column sum up to the number on the bottom.
  3. 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

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):
        if self.s.check() == sat:
            print("Failed to solve.")

puzzle = [

outputfilename = "kakurasu_sol"
ks = KakurasuSolver(9, puzzle, outputfilename)


The solution for above puzzle is given below

Back to top