Open Source Adventures: Episode 70: Crystal Z3 Solver for Nonograms Puzzle
Tags: crystal, z3
Published: 2022-07-06 15:50:37

[Nonograms](https://www.puzzle-nonograms.com/?size=4) is one of more popular puzzles.

* there's a grid of cells, you need do fill some of them
* each row and each column has some hints, each being a list of numbers
* a hint like "2 5 3" means the row (or column) has three groups of filled cells - a group of 2 filled cells, followed by a group of 5 filled cells, followed by a group of 3 filled cells - each group separated by at least one empty cell
* that corresponds to regex `^_*#{2}_+#{5}_+#{3}_+$`, if we take `_` as empty and `#` as filled space

As usual, I recommend playing the puzzle a few times to get a good feel for it. It will make it easier to follow along.

### Plaintext input

The board starts empty, so we don't need any board. We just need column hints, then row hints.

I separate them with a `-` line. Empty line would be more obvious, but the puzzle can legitimately contain an empty hint for row or column (in that case no cell in it is filled).

Here's an example of 25x25 puzzle:

```
4 2 1 2 2
4 1 1 3
4 2 2 3
8 10
6 3 9
3 1 1 9
2 1 1 8
2 1 1 2 2 5
1 1 4 1 3
2 9 6
13 7
4 1 6 4 2
1 1 3 3 3
1 3 1 1 2
2 8 2
5 1 4 2
5 3 1 2
5 2 4
6 2 3
5 1 2
3 4 2
4 2 3 2
6 3 4 3
8 4 1
1 1 4 4
-
6 1 2
1 5 1 3
6 8 3
5 5 10
5 4 9
4 2 9
1 1 5 1
1 3 1 2 2
4 2 1 2
1 1 6 2
1 3 8
10
5 5 3
9 6
4 5 1 5
6 3 2 5
4 1
8
1 6 2 1
4 5 1
5 5 1 1
7 9 1
11 2 2 3
4 6 6
5 6
```

### Solver

```crystal
#!/usr/bin/env crystal

require "z3"

class Nonograms
  @col_hints : Array(Array(Int32))
  @row_hints : Array(Array(Int32))

  def initialize(path)
    col, row = File.read(path).split("-\n", 2)
    @col_hints = col.chomp.split("\n").map{|l| l.split.map(&.to_i)}
    @row_hints = row.chomp.split("\n").map{|l| l.split.map(&.to_i)}
    @xsize = @col_hints.size
    @ysize = @row_hints.size
    @solver = Z3::Solver.new
    @cells = {} of Tuple(Int32, Int32) => Z3::BoolExpr
  end

  def column_cells(x)
    (0...@ysize).map{|y| @cells[{x,y}]}
  end

  def row_cells(y)
    (0...@xsize).map{|x| @cells[{x,y}]}
  end

  def setup_groups(name, hints, cells)
    count = hints.size
    starts = (0...count).map{|i| Z3.int("#{name} start #{i}") }
    ends = (0...count).map{|i| Z3.int("#{name} end #{i}") }

    # Every group is on the board
    count.times do |i|
      @solver.assert starts[i] >= 0
      @solver.assert ends[i] <= cells.size
    end

    # Every group has correct size
    hints.each_with_index do |hint, i|
      @solver.assert starts[i] + hint == ends[i]
    end

    # There is a gap between groups
    (count-1).times do |i|
      @solver.assert starts[i+1] >= ends[i] + 1
    end

    # Each filled cell belongs to one of the groups
    cells.each_with_index do |c, j|
      cell_j_in_group_i = count.times.map{|i| (j >= starts[i]) & (j < ends[i]) }
      # this is fairly awkward and we should probably add Z3.or()
      cell_j_in_any_group = count == 0 ? false : cell_j_in_group_i.reduce{|a,b| a|b}
      @solver.assert c == cell_j_in_any_group
    end
  end

  def call
    # Setup cell variables
    @xsize.times do |x|
      @ysize.times do |y|
        @cells[{x,y}] = Z3.bool("cell #{x},#{y}")
      end
    end

    # Setup groups
    @col_hints.each_with_index do |hints, x|
      setup_groups("c#{x}", hints, column_cells(x))
    end

    @row_hints.each_with_index do |hints, y|
      setup_groups("r#{y}", hints, row_cells(y))
    end

    # Print the solution
    if @solver.satisfiable?
      model = @solver.model
      @ysize.times do |y|
        @xsize.times do |x|
          v = (model[@cells[{x, y}]].to_s == "true")
          if v
            print "#"
          else
            print "."
          end
        end
        print "\n"
      end
    else
      puts "No solution"
    end
  end
end

Nonograms.new(ARGV[0]).call
```

The code is mostly straightforward, however there are some issues:

* `cell_j_in_any_group = count == 0 ? false : cell_j_in_group_i.reduce{|a,b| a|b}` calculations is really ugly - we'd much rather see something like `@solver.assert c == Z3.or(cell_j_in_group_i)` - and same for `Z3.and`, `Z3.mul`, and `Z3.add`
* just like with previous solvers, `Z3::Model#[]` not guaranteeing return type is a problem, and instead of `(model[@cells[{x, y}]].to_s == "true")` we'd much rather have `model[@cells[{x, y}]].to_b` - this is not completely straightforward as `.to_i` will need to return a `BigInt` for Z3 integers and bitvectors (not `Int32`), and there's no good object to return for Z3 reals.

### Result

```
$ ./nonograms 1.txt
...######......#......##.
#..#####.......#......###
######.....########..###.
#####..#####..##########.
#####....####..#########.
.####.....##....#########
...#......#....#####...#.
...#.....###..#...##..##.
....####.##...#......##..
#...#....######......##..
#...###..########........
.........##########......
.......#####..#####...###
.......#########...######
..####..#####.#.....#####
######..###.##......#####
...####.............#....
########.................
#.######..##....#........
...####.#####...........#
...#####.#####..#.......#
.#######.#########......#
###########...##.##...###
####..######.....######..
.......#####.....######..
```

### Story so far

[All the code is on GitHub](https://github.com/taw/open-source-adventures).

### Coming next

I want to do a few more puzzle game solvers, but first I want to improve Crystal Z3 shard to fix the issues I had so far.