Posted on Jul 3, 2022

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