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 `1`

s and `0`

s 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 `\n`

s).

```
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.

## Discussion (0)