## Nonogram puzzle solver using Z3 SMT-solver

This is a sample one, from Wikipedia:

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.