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:
Bfor wall0to4for wall with a hintatozfor 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
Coming next
That's the last Crystal Z3 solver. In the next episode we'll try another technology.