# Solving Numbrix using Z3

Using the fantastic Z3 for fun.
Z3
puzzles
Published

October 25, 2019

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

for i, line in enumerate(re.split("\n", puzzle)):
for j, v in enumerate(re.split(",", line)):
if 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):
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``````