## Nonogram puzzle solver using Z3 SMT-solver

This is a sample one, from Wikipedia:

( https://en.wikipedia.org/wiki/Nonogram )

The source code of my solver: https://github.com/DennisYurichev/yurichev.com/blob/master/blog/nonogram/nonogram_solver.py.

The result:
sat
******** ******* ***** *******
***** **** *** ***
*** *** ** ***
**** *** ** **
*** *** ** **
*** **** ** **
**** ***** **
*** ***** *
**** *** **
*** **** **
**** **** **
*** ****** **
*** ** *** *
**** *** **** **
*** ** *** **
****** *****
**** *****
*** ***
*** ***
* *

How it works (briefly).
Given a row of width 8 and input (or "clue") like [3,2], we create two "islands" of two bitstrings of corresponding
lengths:

00000111
00000011

The whole length of each bitvector/bitstring is 8 (width of row).

We then define another variable: island_shift, for each "island", which defines a count, on which a bitstring is shifted left.
We also calculate limits for each "island": position of each one must not be lower/equal then the position of the previous
"island".

All islands are then merged into one (merged_islands[]) using OR operation:

11100000
00001100
->
11101100

merged_islands[] is a final representation of row - how it will be printed.

Now repeat this all for all rows and all columns.

The final step: make corresponding bits in XXX_merged_islands[] of each row and column to be equal to each other.
In other words, col_merged_islands[] must be equal to row_merged_islands[], but rotated by 90°.

The solver is surprisingly fast even on hard puzzles.

Further work: colored nonograms.

→ [list of blog posts]

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