Solving Kakuro using Z3

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.inp, self.vars = self.load_puzzle(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()])

    def load_puzzle(self, fp):
        X = []
        with(open(fp, "r")) as f:
            for line in f.readlines():
                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
                        self.s.add(And(Distinct(bvars)))
                        self.s.add(And(sum(bvars) == int(r)))
                    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
                        self.s.add(And(Distinct(bvars)))
                        self.s.add(And(sum(bvars) == int(c)))

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