## DEV Community is a community of 892,765 amazing developers

We're a place where coders share, stay up-to-date and grow their careers.

Tomasz Wegrzanowski

Posted on

# 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)
@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*.*
``````

### Coming next

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