DEV Community

Tomasz Wegrzanowski
Tomasz Wegrzanowski

Posted on

3 2

Open Source Adventures: Episode 69: Crystal Z3 Solver for Aquarium Puzzle

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
Enter fullscreen mode Exit fullscreen mode
$ ./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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
.....##...
.###......
......####
...##...##
...###...#
#....#####
##...#....
##........
#.....#...
#...#####.
Enter fullscreen mode Exit fullscreen mode

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.

AWS Security LIVE!

Join us for AWS Security LIVE!

Discover the future of cloud security. Tune in live for trends, tips, and solutions from AWS and AWS Partners.

Learn More

Top comments (0)

A Workflow Copilot. Tailored to You.

Pieces.app image

Our desktop app, with its intelligent copilot, streamlines coding by generating snippets, extracting code from screenshots, and accelerating problem-solving.

Read the docs

👋 Kindness is contagious

Engage with a sea of insights in this enlightening article, highly esteemed within the encouraging DEV Community. Programmers of every skill level are invited to participate and enrich our shared knowledge.

A simple "thank you" can uplift someone's spirits. Express your appreciation in the comments section!

On DEV, sharing knowledge smooths our journey and strengthens our community bonds. Found this useful? A brief thank you to the author can mean a lot.

Okay