## DEV Community

Tomasz Wegrzanowski

Posted on

# Open Source Adventures: Episode 70: Crystal Z3 Solver for Nonograms Puzzle

Nonograms 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

``````#!/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
...######......#......##.
#..#####.......#......###
######.....########..###.
#####..#####..##########.
#####....####..#########.
.####.....##....#########
...#......#....#####...#.
...#.....###..#...##..##.
....####.##...#......##..
#...#....######......##..
#...###..########........
.........##########......
.......#####..#####...###
.......#########...######
..####..#####.#.....#####
######..###.##......#####
...####.............#....
########.................
#.######..##....#........
...####.#####...........#
...#####.#####..#.......#
.#######.#########......#
###########...##.##...###
####..######.....######..
.......#####.....######..
``````

### 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.