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.