Solving nonograms with ruby and Z3

Z3 is quite amazing, and whenever I show it to people on various unconferences response is very enthusiastic, but it desperately needs some tutorials.

I wrote one for sudoku, but sudoku is maybe just a too straightforward example - variables are simply what goes into cells, and constraints are simply game rules. Usually you'll need at least a bit more modelling than that.

So let's try something just a bit more complicated - nonograms:

Nonograms are a puzzle where there's a grid of cells, either filed or empty.

Every row and column has numbers describing cells as seen from its own perspective. So if a row has numbers "2 7" next to it, it means there's a group of 2 filled cells, and then (with at least one empty cell gap) another group of 7 filled cells.

I'm going to refer to both rows and columns as "stripes", as logic for both is exactly the same, so it's simpler to just write it once.

Get the data

So the first thing we do is OCR that image... Just kidding, we'll transcribe it manually, as setting up proper OCR would take longer than that.

Of course in a real solver these numbers would come from somewhere - probably an HTML scrapper, but it could really be OCR, or something else altogether.

class NonogramSolver
  def initialize
    @row_constraints = [
      [3],
      [5],
      [3,1],
      [2,1],
      [3,3,4],
      [2,2,7],
      [6,1,1],
      [4,2,2],
      [1,1],
      [3,1],
      [6],
      [2,7],
      [6,3,1],
      [1,2,2,1,1],
      [4,1,1,3],
      [4,2,2],
      [3,3,1],
      [3,3],
      [3],
      [2,1],
    ]
    @column_constraints = [
      [2],
      [1,2],
      [2,3],
      [2,3],
      [3,1,1],
      [2,1,1],
      [1,1,1,2,2],
      [1,1,3,1,3],
      [2,6,4],
      [3,3,9,1],
      [5,3,2],
      [3,1,2,2],
      [2,1,7],
      [3,3,2],
      [2,4],
      [2,1,2],
      [2,2,1],
      [2,2],
      [1],
      [1],
    ]
    @row_count = @row_constraints.size
    @column_count = @column_constraints.size
    @solver = Z3::Solver.new
  end
end

Setting up cell variables

Z3 variables are basically just Symbols with types, and Z3's boolean sort already has the right range, so we don't need to do anything special. A helper function

For convenience let's write helpers to return row and column of such variables.

None of these functions are strictly necessary and it's totally reasonable to do such calculations where they're needed.

  def cell(x,y)
    Z3.Bool("cell#{x},#{y}")
  end

  def row(y)
    (0...@column_count).map{|x| cell(x,y) }
  end

  def column(x)
    (0...@row_count).map{|y| cell(x,y) }
  end

Express grid constraints as stripe constraints

Every stripe (row or column) is independent, so let's write our grid constraints in terms of constraints over individual stripes.

We're passing unique identifier like "row-4" or column-7 to the following function, as they'll need to setup some variables, which need to be unique, and such meaningful names make debugging easier than just allocating variable names at random.

  def setup_grid_constraints!
    (0...@column_count).each do |x|
      setup_stripe_constraints! "column-#{x}", @column_constraints[x], column(x)
    end

    (0...@row_count).each do |y|
      setup_stripe_constraints! "row-#{y}", @row_constraints[y], row(y)
    end
  end

Constraints for single stripe

Everything we've written so far was trivial, but here comes some real modelling. We have match group size constraints - an array like [4,2,2] with an array of boolean cell variables.

How would we model that? Here's one idea:

• For every group have its starting and ending cell as integer variable
• All starts and ends must fit within stripe size - between 0 and N-1 for stripe with N cells
• Difference between start and end equals group size minus one
• Difference between end of one group and start of the next is at least 2
• Cell is filled (true) if and only if it's between start and end of one of the groups

Here's the code for it:

  def setup_stripe_constraints!(stripe_name, stripe_constraints, stripe)
    group_count = stripe_constraints.size
    group_start = (0...group_count).map{|i| Z3.Int("#{stripe_name}-#{i}-start")}
    group_end = (0...group_count).map{|i| Z3.Int("#{stripe_name}-#{i}-end")}

    # Start and end of each group
    (0...group_count).each do |i|
      @solver.assert (group_start[i] >= 0) & (group_start[i] < stripe.size)
      @solver.assert (group_end[i] >= 0) & (group_end[i] < stripe.size)
      @solver.assert group_end[i] - group_start[i] == stripe_constraints[i] - 1
    end
    # Gap between each group and following group
    (0...group_count).each_cons(2) do |i,j|
      @solver.assert group_start[j] >= group_end[i] + 2
    end
    # Cells
    (0...stripe.size).each do |k|
      cell_in_specific_group = (0...group_count).map{|i|
        (k >= group_start[i]) & (k <= group_end[i])
      }
      @solver.assert stripe[k] == Z3.Or(*cell_in_specific_group)
    end
  end

The obvious alternative would be to make end variable point at cell after last, or to just have one variable for cell position, and do a bit more math.

Print the result

And that's it. Let's print the results, and while at it, why not use some Unicode to spice them up

  def solve!
    setup_grid_constraints!
    if @solver.satisfiable?
      model = @solver.model
      (0...@row_count).each do |y|
        (0...@column_count).each do |x|
          value = model[cell(x,y)].to_s
          print value == "true" ? "\u25FC" : "\u25FB"
        end
        print "\n"
      end
    else
      puts "Nonogram has no solution"
    end
  end

Results

Just as expected.

Next Steps

I'd strongly recommend everyone to play with Z3. Logic puzzles are definitely not its main application, they're just great for showing basic techniques without getting bogged down with details of real world problems.

The gem itself contains a collection of examples and you're definitely welcome to contribute more.

If posts like this one are popular, I can keep writing tutorials more increasingly more complex and realistic problems.