## DEV Community is a community of 892,765 amazing developers

We're a place where coders share, stay up-to-date and grow their careers.

Tomasz Wegrzanowski

Posted on

# Open Source Adventures: Episode 66: Crystal Z3 Solver for Mosaic Puzzle

Mosaic Puzzle is really close to Minesweeper Puzzle we did in the previous episode.

Logically the only difference is that hint cells can also contain mines. And for that reason, instead of "mines" it talks about black and white cells.

The difficulty we'll have will be with the output, not with the solver.

### `shard.yml`

First we need to load Z3:

``````name: mosaic-solver
version: 0.0.1

dependencies:
z3:
github: taw/crystal-z3
``````

### Solver

The solver is almost identical to the one for Minesweeper we did in the previous episode. The only difference in the solver part is that `@vars[{x, y}]?` is included in `neighbourhood(x, y)`, and we no longer assert that hint cells must be empty.

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

require "z3"

class MosaicSolver
@data : Array(Array(Nil | Int32))
@ysize : Int32
@xsize : Int32

def initialize(path)
@data = File.read_lines(path).map{|l| l.chars.map{|c| c.ascii_number? ? c.to_i : nil}}
@ysize = @data.size
@xsize = @data[0].size
@solver = Z3::Solver.new
@vars = {} of Tuple(Int32, Int32) => Z3::BoolExpr
end

def each_coord
@ysize.times do |y|
@xsize.times do |x|
yield(x, y)
end
end
end

def neighbourhood(x, y)
[
@vars[{x, y+1}]?,
@vars[{x, y}]?,
@vars[{x, y-1}]?,
@vars[{x+1, y+1}]?,
@vars[{x+1, y}]?,
@vars[{x+1, y-1}]?,
@vars[{x-1, y+1}]?,
@vars[{x-1, y}]?,
@vars[{x-1, y-1}]?,
].compact
end

def neighbourhood_count(x, y)
neighbourhood(x, y).map{|v| v.ite(1, 0)}.reduce{|a,b| a+b}
end

def call
each_coord do |x, y|
@vars[{x, y}] = Z3.bool("#{x},#{y}")
end
each_coord do |x, y|
c = @data[y][x]
if c
@solver.assert neighbourhood_count(x, y) == c
end
end
...
end
end

solver = MosaicSolver.new(ARGV[0])
solver.call
``````

### Printing solution

OK, let's get to the complicated part, printing the solution. It's complicated because we need to use different colors and still print the number hints.

We could use a fancy library for it, but terminal codes aren't all that complicated, so I just hardcoded them.

``````    if @solver.check
model = @solver.model
@ysize.times do |y|
@xsize.times do |x|
v = (model[@vars[{x, y}]].to_s == "true")
c = @data[y][x] || " "
if v
print "\e[30;104m"
else
print "\e[30;102m"
end
print c
end
print "\e[0m"
print "\n"
end
else
puts "No solution"
end
``````

### Result

Here's what it looks like:

### Coming next

Over the next few episodes I'll code a few more puzzle game solvers in Crystal and Z3.