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
Coming next
Over the next few episodes I'll code a few more puzzle game solvers in Crystal and Z3.
Top comments (0)