Open Source Adventures: Episode 67: Crystal Z3 Solver for Tents Puzzle

Let's do a more complex puzzle - Tents.

Here are the rules:

  • there's a grid of cells, we need to find out which of the cells contain tents
  • puzzle specifies grid size, row hints, column hints, and tree positions
  • every row has a hint how many tents are in that row
  • every column has a hint how many tents are in that column
  • no two tents can touch, not even diagonally
  • each tent belongs to a specific tree it's next to (horizontally or vertically; not diagonally), in a 1:1 correspondence

If you've never played this puzzle, I recommend doing a few small easy puzzles now, it will make the post easier to follow.

Most of the rules are very straightforward to translate to solver code, but the last one will be a bit challenging.

Plaintext representation of the puzzle

Very big puzzles can have multi-digit hints, but for simplicity I'll limit this solver to just hints 0-9.

Top row and left column are for hints. Everything else is . for empty space and T for a tree.

 151613232341607
5.T.T....T.T....
1.T.......T....T
4......T......T.
2...T..T........
4..T........TTT.
2T....T.T.......
2.........T..T..
3..T..........T.
2.T.........T..T
2........T...T..
4....TTT.T.....T
3.T.T..T........
4...........T.T.
1.T.T.T.T....T.T
6.T.........T...

Importer

Of course I'm not really feeling like typing a huge number of random characters, as I'd make mistakes so I wrote an importer to turn Puzzle Team internal format's into our plaintext representation.

#!/usr/bin/env crystal

puzzle = ARGV[0].split(",")
size = (puzzle.size - 1) // 2
top = puzzle[1, size]
left = puzzle[-size..-1]
trees = puzzle[0]
map = trees.chars.map{|c| "." * ['_', *'a'..'z'].index(c).not_nil! }.join("T").scan(/.{#{top.size}}/).map(&.[0])
puts [" #{top.join}\n", left.zip(map).map{|a,b| "#{a}#{b}\n"}.join].join
$ crystal ./import_puzzle 'aadaegdffdbjh__adapbdjbibhcf__aeaabsabaaadaaic,1,5,1,6,1,3,2,3,2,3,4,1,6,0,7,5,1,4,2,4,2,2,3,2,2,4,3,4,1,6'  > 1.txt

The format is very simple. First section is a string of symbols for how much space is there between trees (_ for 0, a for 1, b for 2 etc.), then comma separated hints.

Variables

We definitely need one variable for every space on the grid - true if there's a tent there, false otherwise. This covers most rules except the last one.

For the rule about trees we need additional variable. Number 0-4 for each cell. 0 if there's no tree. 1 if there's a tree with tent to the North, 2 to the East, 3 to the South, and 4 to the West. The exact values don't matter here, as long as we use different values for each direction, so we're going clockwise for simplicity here.

With that, we can get to coding!

Solver

Now that we have the approach, let's write the solver.

#!/usr/bin/env crystal

require "z3"

class TentsSolver
  @ysize : Int32
  @xsize : Int32
  @row_hints : Array(Int32)
  @col_hints : Array(Int32)
  @trees : Array(Array(Bool))

  def initialize(path)
    lines = File.read_lines(path)
    @col_hints = lines.shift[1..-1].chars.map(&.to_i)
    @xsize = @col_hints.size
    @row_hints = lines.map(&.[0].to_i)
    @ysize = @row_hints.size
    @trees = lines.map{|l| l[1..-1].chars.map{|c| c == 'T'}}
    @solver = Z3::Solver.new
    @tent_vars = {} of Tuple(Int32, Int32) => Z3::BoolExpr
    @tree_vars = {} of Tuple(Int32, Int32) => Z3::IntExpr
  end

  def each_coord
    @xsize.times do |x|
      @ysize.times do |y|
        yield(x, y)
      end
    end
  end

  def row_tent_count(y)
    (0...@xsize).map{|x| @tent_vars[{x,y}].ite(1, 0)}.reduce{|a,b| a+b}
  end

  def col_tent_count(x)
    (0...@ysize).map{|y| @tent_vars[{x,y}].ite(1, 0)}.reduce{|a,b| a+b}
  end

  def neighbourhood(x,y)
    [
      @tent_vars[{x, y+1}]?,
      @tent_vars[{x, y-1}]?,
      @tent_vars[{x+1, y+1}]?,
      @tent_vars[{x+1, y}]?,
      @tent_vars[{x+1, y-1}]?,
      @tent_vars[{x-1, y+1}]?,
      @tent_vars[{x-1, y}]?,
      @tent_vars[{x-1, y-1}]?,
    ].compact
  end

  def call
    # Initialize tent variables
    each_coord do |x, y|
      @tent_vars[{x,y}] = Z3.bool("tent #{x},#{y}")
    end

    # Initialize tree variables
    each_coord do |x, y|
      @tree_vars[{x,y}] = v = Z3.int("tree #{x},#{y}")
      if @trees[y][x]
        @solver.assert v >= 1
        @solver.assert v <= 4
      else
        @solver.assert v == 0
      end
    end

    # Row hints are correct
    @ysize.times do |y|
      @solver.assert row_tent_count(y) == @row_hints[y]
    end

    # Col hints are correct
    @xsize.times do |x|
      @solver.assert col_tent_count(x) == @col_hints[x]
    end

    # No two tents are next to each other
    each_coord do |x,y|
      neighbourhood(x,y).each do |nv|
        @solver.assert @tent_vars[{x,y}].implies(~nv)
      end
    end

    # Every tree has corresponding tent
    each_coord do |x,y|
      v = @tree_vars[{x,y}]
      @solver.assert (v == 1).implies(@tent_vars[{x,y-1}]? || false) # N
      @solver.assert (v == 2).implies(@tent_vars[{x+1,y}]? || false) # E
      @solver.assert (v == 3).implies(@tent_vars[{x,y+1}]? || false) # S
      @solver.assert (v == 4).implies(@tent_vars[{x-1,y}]? || false) # W
    end

    # Now print the solution
    if @solver.check
      model = @solver.model
      @ysize.times do |y|
        @xsize.times do |x|
          v = (model[@tent_vars[{x, y}]].to_s == "true")
          if @trees[y][x]
            print "T"
          elsif v
            print "*"
          else
            print "."
          end
        end
        print "\n"
      end
    else
      puts "No solution"
    end
  end
end

TentsSolver.new(ARGV[0]).call

The code is mostly straightforward. A few interesting parts would be:

  • Z3 handles _.implies(false) just fine, so we don't need to do bounds checks, but we still need to convert nil to false, with _.implies(@tent_vars[{x,y-1}]? || false) etc.
  • input parsing contains some fancy Crystal tricks like lines.map(&.[0].to_i)
  • to make type checker happy, we need to initialize empty hashes for variables, like @tent_vars = {} of Tuple(Int32, Int32) => Z3::BoolExpr - this requires a lot less logic around bounds check than using nested arrays would

Result

$ ./tents 1.txt
.T*T*...T*T.*.*
.T....*..T....T
.*.*..T..*...T*
...T..T*....*..
..T*.*....*TTT*
T*...T.T....*..
.......*.T*.T..
.*T*.........T*
.T......*..T*.T
......*.T...T.*
.*.*TTT.T*.*..T
.T.T.*T*......*
.*.*......*T*T.
.T.T.T.T*...T.T
*T.*.*....*T*.*

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.