Aquarium is a puzzle with following rules:
- there's a grid of cells, belonging to various water containers
- each cell can contain water or not
- each container is filled to some level, that is - if a cell in a container has water, then every cell in the same container that's at the same level or below also has water
- there are row and column hints specifying how many cells in given row or column are filled
I recommend playing it a few times to get familiar with the puzzle. That will make following the post easier.
Importer
As usual, I have no patience for manually typing all the characters of a big puzzle, and it would be very error prone, so I wrote an importer that converts it from Puzzle Team's internal format.
#!/usr/bin/env crystal
hints, board = ARGV[0].split(";", 2)
hints = hints.split("_")
size = hints.size // 2
top = hints[0, size]
left = hints[size, size]
board = board.split(",").map{|c| (96+c.to_i).chr}.join.scan(/.{#{size}}/).map(&.[0])
puts [" #{top.join}\n\n", left.zip(board).map{|a,b| "#{a} #{b}\n"}.join].join
$ ./import_puzzle '5_3_1_3_3_5_5_3_4_4_2_3_4_4_4_6_3_2_2_6;1,1,1,1,2,3,3,4,4,5,1,6,6,6,2,7,4,4,5,5,1,8,8,2,2,7,4,4,5,9,10,10,10,11,2,7,12,12,9,9,13,13,10,11,11,11,12,14,14,9,15,13,10,10,16,12,12,12,12,12,15,13,10,10,16,12,17,17,17,17,15,13,10,10,16,18,18,18,18,17,19,10,10,16,16,20,18,17,17,17,19,10,10,16,20,20,18,18,18,17' > 1.txt
Plaintext input
And here's the result:
5313355344
2 aaaabccdde
3 afffbgddee
4 ahhbbgddei
4 jjjkbgllii
4 mmjkkklnni
6 omjjplllll
3 omjjplqqqq
2 omjjprrrrq
2 sjjpptrqqq
6 sjjpttrrrq
To keep it a little less busy, I added extra space column and row between hints and the board.
Solver
Here's the solver:
#!/usr/bin/env crystal
require "z3"
class AquariumSolver
@col_hints : Array(Int32)
@row_hints : Array(Int32)
@board : Array(Array(Char))
@containers : Set(Char)
def initialize(path)
lines = File.read_lines(path)
@col_hints = lines[0][2..].chars.map(&.to_i)
@xsize = @col_hints.size
@row_hints = lines[2..].map(&.[0].to_i)
@ysize = @row_hints.size
@board = lines[2..].map{|l| l[2..].chars}
@containers = @board.flatten.to_set
@solver = Z3::Solver.new
@cells = {} of Tuple(Int32, Int32) => Z3::BoolExpr
@water_levels = {} of Char => Z3::IntExpr
end
def each_coord
@xsize.times do |x|
@ysize.times do |y|
yield(x, y)
end
end
end
def row_cell_count(y)
(0...@xsize).map{|x| @cells[{x,y}].ite(1, 0)}.reduce{|a,b| a+b}
end
def col_cell_count(x)
(0...@ysize).map{|y| @cells[{x,y}].ite(1, 0)}.reduce{|a,b| a+b}
end
def call
# Initialize cell variables
each_coord do |x, y|
@cells[{x,y}] = Z3.bool("cell #{x},#{y}")
end
# Initialize water level variables
# We could restrict it more tightly to make solution unambiguous
# Right now container at levels 4-6 can have any level 0-10
# even though 0-4 means same (all full), and 6-10 means same (all empty)
@containers.each do |c|
@water_levels[c] = v = Z3.int("level #{c}")
@solver.assert v >= 0
@solver.assert v <= @ysize
end
# All cells in each container have correct water level
each_coord do |x, y|
c = @board[y][x]
@solver.assert @cells[{x,y}] == (y >= @water_levels[c])
end
# Row hints are correct
@ysize.times do |y|
@solver.assert row_cell_count(y) == @row_hints[y]
end
# Col hints are correct
@xsize.times do |x|
@solver.assert col_cell_count(x) == @col_hints[x]
end
# Print the solution
if @solver.satisfiable?
model = @solver.model
@ysize.times do |y|
@xsize.times do |x|
v = (model[@cells[{x, y}]].to_s == "true")
if v
print "#"
else
print "."
end
end
print "\n"
end
else
puts "No solution"
end
end
end
AquariumSolver.new(ARGV[0]).call
The solver generally uses techniques already covered by previous solvers.
- water level check is a bit unintuitive as we count from 0 on top (the way plaintext input is indexed) instead of 0 on bottom (as would make more sense semantically)
- for simplicity, we allow containers to have any water level from 0 to MAX - even water levels above top or below bottom of the container - this creates some ambiguity in the solution, and we count do tighter bounds. But since we only care about cells in results, not water levels, this still works fine.
Result
$ ./aquarium 1.txt
.....##...
.###......
......####
...##...##
...###...#
#....#####
##...#....
##........
#.....#...
#...#####.
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)