## Numberlink (AKA Flow Free) puzzle as a MaxSAT problem + toy PCB router

Let's revisit my solution for Numberlink (AKA Flow Free) puzzle written for Z3Py.

What if holes in the puzzle exist?
Can we make all paths as short as possible?

I've rewritten the puzzle solver using my own SAT library Xu.py
and now I use Open-WBO MaxSAT solver, see the source code, which is almost the same:
https://github.com/DennisYurichev/yurichev.com/blob/master/blog/numberlink_MaxSAT/numberlink_WBO.py.

But now we "maximize" number of empty cells:

┏1 5┏━3┏━6
┃ ┏┛┃ ┏┛ 2
┃5┛ ┃ ┃ ┃
┗━┓ ┃┏┛ ┏┛
7 ┗┓┃┃ ┏┛
┗━┓┃3┃ 2
4┃┃6┛┏━━┓
┏┛┃┃┏━┛┏8┃
┃ ┃19┏7┃┏┛
4 ┗━━┛ 89

This is a solution with shortest possible paths. Others are possible, but their sum wouldn't be shorter.
This is like toy PCB routing.

What if we comment the **s.fix_soft_always_true(cell_is_empty[r][c], 1)** line?

┏1 5┓ 3┓┏6
┃┏┓┏┛ ┏┛┃2
┃5┗┛┏━┛ ┃┃
┗┓ ┗┓ ┃┃
7┗━┓ ┃┏━┛┃
┗━┓┃3┛┃2━┛
4┃┃6━┛┏━┓
┃┃┃┏━━┛8┃
┃┃19┏7┏┛┃
4┛┗━━┛ 89┛

Lines 5 and 3 "roaming" chaotically, but the solution is correct, under given constraints.

The files: https://github.com/DennisYurichev/yurichev.com/tree/master/blog/numberlink_MaxSAT.

→ [list of blog posts]

Please drop me email about any bug(s) and suggestion(s): *dennis(@)yurichev.com*.