Solving Numbrix using Z3

Numbrix

Just fill in the puzzle so the consecutive numbers follow a horizontal or vertical path (no diagonals).

Here is a hard numbrix puzzle

Python code using Z3

from z3 import *
import re
from itertools import combinations

def Abs(x):
    return If(x >=0, x, -x)

class NumbricksSolver:
    def __init__(self, n):
        self.n = n
        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(1 <= self.X[i][j], self.X[i][j]<= n*n) for i in range(n) for j in range(n)])
        self.s.add([And(Distinct([self.X[i][j] for i in range(n) for j in range(n)]))])
        for i in range(n):
            for j in range(n):
                ns = []
                if (i - 1) >= 0:
                    ns.append(self.X[i-1][j])
                if (i + 1) < n:
                    ns.append(self.X[i+1][j])
                if (j - 1) >= 0:
                    ns.append(self.X[i][j-1])
                if (j + 1) < n:
                    ns.append(self.X[i][j+1])
                c_n1_ne = Or(*[And(*[Abs(self.X[i][j]-nb)==1 for nb in nbs])
                            for nbs in combinations(ns, 2)])
                c_1_or_e = Or(*[Abs(self.X[i][j]-nb)==1 for nb in ns])
                self.s.add(If(self.X[i][j] == 1, c_1_or_e, If(self.X[i][j] == n*n, c_1_or_e, c_n1_ne)))

    def load_puzzle(self, puzzle):
        for i, line in enumerate(re.split("\n", puzzle)):
            for j, v in enumerate(re.split(",", line)):
                if v != "_":
                    self.s.add(And(self.X[i][j] == int(v)))

    def output_solution(self):
        m = self.s.model()
        for i in range(self.n):
            print("  ".join(['{:>2}'.format(str(m.evaluate(self.X[i][j]))) 
                for j in range(self.n)]))
            print("\n")

    def solve(self, puzzle):
        self.load_puzzle(puzzle)
        if self.s.check() == sat:
            self.output_solution()
        else:
            print(self.s)
            print("Failed to solve.")

puzzle = '''9,_,11,_,19,_,77,_,73
_,_,_,_,_,_,_,_,_
7,_,_,_,_,_,_,_,71
_,_,_,_,_,_,_,_,_
31,_,_,_,_,_,_,_,67
_,_,_,_,_,_,_,_,_
35,_,_,_,_,_,_,_,57
_,_,_,_,_,_,_,_,_
37,_,41,_,45,_,47,_,55'''

ns = NumbricksSolver(9)
ns.solve(puzzle)

Solution

Here is the solution to the above puzzle

9  10  11  18  19  78  77  74  73

 8  13  12  17  20  79  76  75  72

 7  14  15  16  21  80  81  70  71

 6   5   4   3  22  63  64  69  68

31  30  29   2  23  62  65  66  67

32  33  28   1  24  61  60  59  58

35  34  27  26  25  50  51  52  57

36  39  40  43  44  49  48  53  56

37  38  41  42  45  46  47  54  55