Open Source Adventures: Episode 65: Crystal Z3 Solver for Minesweeper Puzzle
Let's write some puzzle solvers. This time - Minesweeper Puzzle.
Minesweeper puzzle differs from the Minesweeper game in that a bunch of mine hints are provided from the start. In the game you start with the empty board, and get hints revealed as game goes.
Plaintext Input
With these puzzles, a very important thing is having some sort of convenient plaintext input format. Some of the puzzles are simple in theory, and might even look simple on paper, but just dealing with I/O is a lot of work.
Fortunately Minesweeper is really simple:
1_2__0__1_
_2__2__2_1
____22____
__42__21_1
2____21___
22__2____2
__1__11___
_2__3__23_
___5_2__3_
1____2_3_1
Boxes with hints are represented by a number. The only complexity is dealing with empty cells without hints - it's tempting to use spaces, but meaningful trailing spaces cause all sort of trouble, so it's better to use a placeholder character like _ or . instead.
Such format is very easy to parse:
@data : Array(Array(Nil | Int32))
@data = File.read_lines(path).map{|l| l.chars.map{|c| c.ascii_number? ? c.to_i : nil}}
One thing that's tempting is c =~ /\d/ like in Ruby, but that doesn't work in Crystal, as c is Char not String. In this case .ascii_number? is totally fine.
Variables
Variables for Minesweeper puzzle are very obvious - every cell has a boolean - true if there's a mine, false if not.
The more obvious structure to hold them is a nested array Array(Array(Z3::BoolExpr)), but if we did that, getting all neighbours of given cell would require a lot of border checks.
@vars = {} of Tuple(Int32, Int32) => Z3::BoolExpr
shard.yml
Let's get started, by importing Z3 library:
name: minesweeper-solver
version: 0.0.1
dependencies:
z3:
github: taw/crystal-z3
Solver Structure
We could add a check that some argument has been passed, and print a nice error message, but I'm skipping it for simplicity:
#!/usr/bin/env crystal
require "z3"
class MinesweeperSolver
@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
...
end
solver = MinesweeperSolver.new(ARGV[0])
solver.call
Initialize variables
To start solving, we can put all variables in the Hash.
Most of the puzzles follow a grid. I like using helper methods like each_coord to avoid repeating double nested loops.
def each_coord
@ysize.times do |y|
@xsize.times do |x|
yield(x, y)
end
end
end
def call
each_coord do |x, y|
@vars[{x, y}] = Z3.bool("#{x},#{y}")
end
...
end
Add constraints
There's only one type of constraint - if a cell is a hint cell, then it cannot contain a mine, and number of mines around it equals the hint.
Because we keep variables in a double-indexed Hash, this makes neighbourhood method really easy.
Before adding numbers, we need to tell Z3 to convert booleans into 1s and 0s with .ite (if-then-else). It's basically Z3 equivalent of v ? 1 : 0, except we cannot overload ?: operator.
def neighbourhood(x, y)
[
@vars[{x-1, y-1}]?,
@vars[{x-1, y}]?,
@vars[{x-1, y+1}]?,
@vars[{x, y-1}]?,
@vars[{x, 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|
c = @data[y][x]
if c
@solver.assert neighbourhood_count(x, y) == c
@solver.assert ~@vars[{x,y}]
end
end
...
end
Print solution
Now Z3 can handle the solving, and all we need to do is print the solution.
As Z3::Models#[] isn't fully typed yet, Crystal Z3 doesn't quite know what will be returned (it's Z3::BoolExpr). To keep things simple, I use .to_s == "true" to see if variable is true or not. This could definitely be improved.
We can't use each_coord here as we need to do something at end of each line (print \ns).
def call
...
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 c
print c
elsif v
print "*"
else
print " "
end
end
print "\n"
end
else
puts "No solution"
end
end
Solver in action
Here's an example of solver in action:
$ ./minesweeper.cr 1.txt
1*2* 0 1
2 2 2*1
* *22*
*42 *21 1
2* *21 *
22 2 *2
* 1 *11*
2 *3 23*
*5*2 *3
1*** 2*3*1
Full Solver Code
And here's the complete solver:
#!/usr/bin/env crystal
require "z3"
class MinesweeperSolver
@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-1, y-1}]?,
@vars[{x-1, y}]?,
@vars[{x-1, y+1}]?,
@vars[{x, y-1}]?,
@vars[{x, 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
@solver.assert ~@vars[{x,y}]
end
end
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 c
print c
elsif v
print "*"
else
print " "
end
end
print "\n"
end
else
puts "No solution"
end
end
end
solver = MinesweeperSolver.new(ARGV[0])
solver.call
Story so far
Coming next
Over the next few episodes I'll code a few more puzzle game solvers in Crystal and Z3.