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 convertniltofalse, 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
Coming next
Over the next few episodes I'll code a few more puzzle game solvers in Crystal and Z3.
Top comments (0)