Solving Kakurasu using Z3

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:

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
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