DEV Community

Tomasz Wegrzanowski
Tomasz Wegrzanowski

Posted on

Open Source Adventures: Episode 74: Crystal Z3 Solver for Light Up Puzzle

This is the final episode with Crystal Z3 solvers, at least for now.

In previous episode I showed how to solve Lights Up puzzle with math, now it's time to write a Crystal Z3 solver.

Light Up (Akari) is a simple puzzle with following rules:

  • there's a grid of cells
  • some cells are wall cells
  • your task is to place light bulbs in some of the cells
  • light spreads horizontally and vertically from light bulbs, but it doesn't pass through walls
  • all cells must be illuminated
  • no light bulbs can shine on any other light bulb
  • some wall cells have hints on them (0-4), indicating how many light bulbs are directly neighboring the wall cell, horizontally or vertically

I recommend playing it a few times to get familiar with the puzzle.

Importer

As usual, I have no patience to manually enter a big puzzle. Fortunately Puzzle Team's internal format is very simple:

  • B for wall
  • 0 to 4 for wall with a hint
  • a to z for a sequence of 1-26 empty spaces

Here's the script:

#!/usr/bin/env crystal

puzzle = ARGV[0].gsub(/[a-z]/){|c| "." * (c[0].ord - 96)}.gsub("B", "#")
size = (puzzle.size ** 0.5).to_i

puzzle.chars.each_slice(25) do |slice|
  puts slice.join
end
Enter fullscreen mode Exit fullscreen mode

Which we can use by just passing the puzzle string as argument:

$ ./import_puzzle aBaB0fBfBBbBBaBaBaB1b10aBb0B1d2BaBBBBcB11cBe0BBBBBbBBcBgB0hBb2d0i1e1BBaBe1bBaBdBdBa1aBbBaBb2a3b2eB2f2e0g2a0aBcBjBaBdBb11bBaBb1pBb2a1dBa0cBb1Bk2fBfBc3Bb0cBaBb2aBb0a1cBbBBc1fBf2kB2b0cBa1dBa1bBp0bBa0b11b2d0a1j1cBaBaBgBe1f11e3b1aBb1aBb1aBaBd1dBa3bBe0a1BBe1i0dBbBhBBg1cBBbB1BB11e0c0BBcBBBBaB0dB1BbBaB2bB0aBaBaBBbBBfBfBBaBa
Enter fullscreen mode Exit fullscreen mode

Here's the result:

.#.#0......#......##..##.
#.#.#1..10.#..0#1....2#.#
###...#11...#.....0#####.
.##...#.......#0........#
..2....0.........1.....1#
#.#.....1..#.#....#....#.
1.#..#.#..2.3..2.....#2..
....2.....0.......2.0.#..
.#..........#.#....#..11.
.#.#..1................#.
.2.1....#.0...#..1#......
.....2......#......#...3#
..0...#.#..2.#..0.1...#..
##...1......#......2.....
......#2..0...#.1....#.1.
.#................0..#.0.
.11..2....0.1..........1.
..#.#.#.......#.....1....
..11.....3..1.#..1.#..1.#
.#....1....#.3..#.....0.1
##.....1.........0....#..
#........##.......1...##.
.#1##11.....0...0##...###
#.#0....#1#..#.#2..#0.#.#
.##..##......#......##.#.
Enter fullscreen mode Exit fullscreen mode

Solver

Here's the code:

#!/usr/bin/env crystal

require "z3"

class LightUp
  @xsize : Int32

  def initialize(path)
    @board = File.read_lines(path)
    @ysize = @board.size
    @xsize = @board[0].size
    @solver = Z3::Solver.new
    @cells = {} of Tuple(Int32, Int32) => Z3::BoolExpr
    @horizontal = {} of Tuple(Int32, Int32) => Z3::BoolExpr
    @vertical = {} of Tuple(Int32, Int32) => Z3::BoolExpr
    @members = {} of Z3::BoolExpr => Array(Z3::BoolExpr)
    @members.compare_by_identity
  end

  def each_coord
    @ysize.times do |y|
      @xsize.times do |x|
        yield(x, y)
      end
    end
  end

  def neighbours_count(x, y)
    Z3.add(
      [
        @cells[{x+1,y}]?,
        @cells[{x-1,y}]?,
        @cells[{x,y+1}]?,
        @cells[{x,y-1}]?,
      ].compact.map{|v| v.ite(1,0)}
    )
  end

  def empty?(x, y)
    @board[y][x] == '.'
  end

  # Everything outside the board is a wall
  def empty_left?(x, y)
    x != 0 && empty?(x-1, y)
  end

  def empty_top?(x, y)
    y != 0 && empty?(x, y-1)
  end

  def call
    # Setup cell variables
    each_coord do |x,y|
      @cells[{x,y}] = v = Z3.bool("cell #{x},#{y}")
    end

    # Setup walls and hints
    each_coord do |x,y|
      c = @board[y][x]
      v = @cells[{x,y}]
      if c != '.'
        @solver.assert ~v
      end
      if c.ascii_number?
        @solver.assert neighbours_count(x, y) == c.to_i
      end
    end

    # Setup horizontal group variables
    each_coord do |x, y|
      next unless empty?(x, y)
      if empty_left?(x, y)
        # continue existing group
        @horizontal[{x,y}] = @horizontal[{x-1,y}]
      else
        # start a new group
        @horizontal[{x,y}] = Z3.bool("h #{x},#{y}")
        @members[@horizontal[{x,y}]] = [] of Z3::BoolExpr
      end
      @members[@horizontal[{x,y}]] << @cells[{x,y}]
    end

    # Setup vertical group variables
    each_coord do |x, y|
      next unless empty?(x, y)
      if empty_top?(x, y)
        # continue existing group
        @vertical[{x,y}] = @vertical[{x,y-1}]
      else
        # start a new group
        @vertical[{x,y}] = Z3.bool("v #{x},#{y}")
        @members[@vertical[{x,y}]] = [] of Z3::BoolExpr
      end
      @members[@vertical[{x,y}]] << @cells[{x,y}]
    end

    # Every cell sees a light - either in its horizontal or vertical group (or both)
    each_coord do |x, y|
      next unless empty?(x, y)
      @solver.assert(@horizontal[{x,y}] | @vertical[{x,y}])
    end

    # Group has a light if any of its members has a light
    @members.each do |var, members|
      @solver.assert var == Z3.or(members)
    end

    # No two lights see each other = no group has more than one light
    @members.each do |var, members|
      @solver.assert Z3.add(members.map{|v| v.ite(1,0)}) <= 1
    end

    if @solver.satisfiable?
      model = @solver.model
      @ysize.times do |y|
        @xsize.times do |x|
          c = @board[y][x]
          if c == '.'
            v = model[@cells[{x,y}]].to_b
            print v ? "*" : "."
          else
            print c
          end
        end
        print "\n"
      end
    else
      puts "No solution"
    end
  end
end

LightUp.new(ARGV[0]).call
Enter fullscreen mode Exit fullscreen mode

Cost of overriding ==

Most of it follows the math I showed the previous episode. The most interesting thing code-wise is Hash indexed by Z3::BoolExpr. As Z3::BoolExpr overrides == to return Z3::BoolExprs (instead of Bools) it's not really Hash-compatible type. So instead we call @members.compare_by_identity to switch to comparing by object_id, which is good enough for this use case, but not in general. For example if we wanted a Hash indexed by Tuple(Z3::BoolExpr, Z3::BoolExpr), a totally reasonable design, that trick wouldn't work.

I'm not quite sure if it's possible to make such objects Hash-able, there's just significant cost of the kind of == overrides I'm doing. If we did Z3.equal(a, b), or solver.assert_equal(a, b), we'd not have any such problems, but then the expressions would look a lot worse. It's a API design judgment call.

Result

$ ./light_up 2.txt
...*.
#*1.0
*.###
Enter fullscreen mode Exit fullscreen mode
$ ./light_up 1.txt
*#*#0.*....#....*.##.*##*
#*#.#1.*10.#*.0#1...*2#*#
###..*#11..*#*....0#####*
*##...#.*.....#0.......*#
.*2*...0........*1.*...1#
#.#...*.1.*#*#.*..#...*#.
1.#.*#.#*.2*3.*2..*..#2*.
*...2.....0.*.....2.0.#..
.#..*.......#.#...*#.*11*
.#.#.*1..........*.....#.
.2*1....#.0.*.#..1#....*.
.*...2*.....#*.....#..*3#
..0..*#.#.*2*#..0.1*..#*.
##...1.*....#.*....2*....
..*...#2*.0.*.#.1*...#*1.
.#.........*......0..#.0.
*11*.2*...0.1*.........1*
..#.#*#..*....#....*1....
.*11...*.3*.1.#.*1.#..1*#
.#.*..1..*.#*3*.#.*...0.1
##....*1.....*...0..*.#.*
#.*......##....*..1*..##.
*#1##11*....0...0##..*###
#*#0.*..#1#*.#.#2*.#0.#*#
*##.*##..*...#..*...##*#*
Enter fullscreen mode Exit fullscreen mode

Story so far

All the code is on GitHub.

Coming next

That's the last Crystal Z3 solver. In the next episode we'll try another technology.

Top comments (0)