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

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

$ ./import_puzzle aBaB0fBfBBbBBaBaBaB1b10aBb0B1d2BaBBBBcB11cBe0BBBBBbBBcBgB0hBb2d0i1e1BBaBe1bBaBdBdBa1aBbBaBb2a3b2eB2f2e0g2a0aBcBjBaBdBb11bBaBb1pBb2a1dBa0cBb1Bk2fBfBc3Bb0cBaBb2aBb0a1cBbBBc1fBf2kB2b0cBa1dBa1bBp0bBa0b11b2d0a1j1cBaBaBgBe1f11e3b1aBb1aBb1aBaBd1dBa3bBe0a1BBe1i0dBbBhBBg1cBBbB1BB11e0c0BBcBBBBaB0dB1BbBaB2bB0aBaBaBBbBBfBfBBaBa

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.#.#
.##..##......#......##.#.

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

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
*.###

$ ./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.#*#
*##.*##..*...#..*...##*#*

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.