Open Source Adventures: Episode 65: Crystal Z3 Solver for Minesweeper Puzzle
Tags: crystal, z3
Published: 2022-07-03 10:16:07

Let's write some puzzle solvers. This time - [Minesweeper Puzzle](https://www.puzzle-minesweeper.com/minesweeper-10x10-easy/).

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:

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

```crystal
@vars = {} of Tuple(Int32, Int32) => Z3::BoolExpr
```

### `shard.yml`

Let's get started, by importing Z3 library:

```yml
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:

```crystal
#!/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.

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

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

```crystal
  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:

```crystal
#!/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

[All the code is on GitHub](https://github.com/taw/open-source-adventures).

### Coming next

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