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:

Story so far

All the code is on GitHub.

Coming next

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