Open Source Adventures: Episode 69: Crystal Z3 Solver for Aquarium Puzzle
Tags: crystal, z3
Published: 2022-07-06 00:43:27

[Aquarium](https://www.puzzle-aquarium.com/?size=4) 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.

```crystal
#!/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:

```crystal
#!/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

[All the code is on GitHub](https://github.com/taw/open-source-adventures).

### Coming next

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