DEV Community

Tomasz Wegrzanowski
Tomasz Wegrzanowski

Posted on

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
Enter fullscreen mode Exit fullscreen mode

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}}
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

shard.yml

Let's get started, by importing Z3 library:

name: minesweeper-solver
version: 0.0.1

dependencies:
  z3:
    github: taw/crystal-z3
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

Story so far

All the code is on GitHub.

Coming next

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

Top comments (0)