## Solving Numberlink (AKA Flow Free) puzzle using Z3

This time, Masahiro Sakai has helped me, who also have numberlink puzzle solver in his toysolver.

You probably saw Flow Free puzzle:

I'll stick to Numberlink version of the puzzle. This is the example puzzle from Wikipedia:

This is solved:

The code:

#!/usr/bin/env python
# -*- coding: utf-8 -*-

from z3 import *

puzzle=["   4   ",
" 3  25 ",
"   31  ",
"   5   ",
"       ",
"  1    ",
"2   4  "]

width=len(puzzle[0])
height=len(puzzle)

# number for each cell:
cells=[[Int('cell_r%d_c%d' % (r,c)) for c in range(width)] for r in range(height)]

# connections between cells. L means the cell has connection with cell at left, etc:
L=[[Bool('L_r%d_c%d' % (r,c)) for c in range(width)] for r in range(height)]
R=[[Bool('R_r%d_c%d' % (r,c)) for c in range(width)] for r in range(height)]
U=[[Bool('U_r%d_c%d' % (r,c)) for c in range(width)] for r in range(height)]
D=[[Bool('D_r%d_c%d' % (r,c)) for c in range(width)] for r in range(height)]

s=Solver()

# U for a cell must be equal to D of the cell above, etc:
for r in range(height):
for c in range(width):
if r!=0:
if r!=height-1:
if c!=0:
if c!=width-1:

# yes, I know, we have 4 bools for each cell at this point, and we can half this number,
# but anyway, for the sake of simplicity, this could be better.

for r in range(height):
for c in range(width):
t=puzzle[r][c]
if t==' ':
# puzzle has space, so degree=2, IOW, this cell must have 2 connections, no more, no less.
# enumerate all possible L/R/U/D booleans. two of them must be True, others are False.
t=[]
t.append(And(L[r][c], R[r][c], Not(U[r][c]), Not(D[r][c])))
t.append(And(L[r][c], Not(R[r][c]), U[r][c], Not(D[r][c])))
t.append(And(L[r][c], Not(R[r][c]), Not(U[r][c]), D[r][c]))
t.append(And(Not(L[r][c]), R[r][c], U[r][c], Not(D[r][c])))
t.append(And(Not(L[r][c]), R[r][c], Not(U[r][c]), D[r][c]))
t.append(And(Not(L[r][c]), Not(R[r][c]), U[r][c], D[r][c]))
else:
# puzzle has number, add it to cells[][] as a constraint:
# cell has degree=1, IOW, this cell must have 1 connection, no more, no less
# enumerate all possible ways:
t=[]
t.append(And(L[r][c], Not(R[r][c]), Not(U[r][c]), Not(D[r][c])))
t.append(And(Not(L[r][c]), R[r][c], Not(U[r][c]), Not(D[r][c])))
t.append(And(Not(L[r][c]), Not(R[r][c]), U[r][c], Not(D[r][c])))
t.append(And(Not(L[r][c]), Not(R[r][c]), Not(U[r][c]), D[r][c]))

# if L[][]==True, cell's number must be equal to the number of cell at left, etc:
if c!=0:
if c!=width-1:
if r!=0:
if r!=height-1:

# L/R/U/D at borders sometimes must be always False:
for r in range(height):

for c in range(width):

# print solution:

print s.check()
m=s.model()

print ""

for r in range(height):
for c in range(width):
print m[cells[r][c]],
print ""

print ""

for r in range(height):
for c in range(width):
t=""
t=t+("L" if str(m[L[r][c]])=="True" else " ")
t=t+("R" if str(m[R[r][c]])=="True" else " ")
t=t+("U" if str(m[U[r][c]])=="True" else " ")
t=t+("D" if str(m[D[r][c]])=="True" else " ")
print t+"|",
print ""

print ""

for r in range(height):
row=""
for c in range(width):
t=puzzle[r][c]
if t==' ':
tl=(True if str(m[L[r][c]])=="True" else False)
tr=(True if str(m[R[r][c]])=="True" else False)
tu=(True if str(m[U[r][c]])=="True" else False)
td=(True if str(m[D[r][c]])=="True" else False)

if tu and td:
row=row+"┃"
if tr and td:
row=row+"┏"
if tr and tu:
row=row+"┗"
if tl and td:
row=row+"┓"
if tl and tu:
row=row+"┛"
if tl and tr:
row=row+"━"
else:
row=row+t
print row



The solution:

sat

2 2 2 4 4 4 4
2 3 2 2 2 5 4
2 3 3 3 1 5 4
2 5 5 5 1 5 4
2 5 1 1 1 5 4
2 5 1 5 5 5 4
2 5 5 5 4 4 4

R D| LR  | L  D|  R  | LR  | LR  | L  D|
UD|    D|  RU | LR  | L   |    D|   UD|
UD|  RU | LR  | L   |    D|   UD|   UD|
UD|  R D| LR  | L   |   UD|   UD|   UD|
UD|   UD|  R D| LR  | L U |   UD|   UD|
UD|   UD|   U |  R D| LR  | L U |   UD|
U |  RU | LR  | L U |  R  | LR  | L U |

┏━┓4━━┓
┃3┗━25┃
┃┗━31┃┃
┃┏━5┃┃┃
┃┃┏━┛┃┃
┃┃1┏━┛┃
2┗━┛4━┛