Nonograms is one of more popular puzzles.
- there's a grid of cells, you need do fill some of them
- each row and each column has some hints, each being a list of numbers
- a hint like "2 5 3" means the row (or column) has three groups of filled cells - a group of 2 filled cells, followed by a group of 5 filled cells, followed by a group of 3 filled cells - each group separated by at least one empty cell
- that corresponds to regex
^_*#{2}_+#{5}_+#{3}_+$, if we take_as empty and#as filled space
As usual, I recommend playing the puzzle a few times to get a good feel for it. It will make it easier to follow along.
Plaintext input
The board starts empty, so we don't need any board. We just need column hints, then row hints.
I separate them with a - line. Empty line would be more obvious, but the puzzle can legitimately contain an empty hint for row or column (in that case no cell in it is filled).
Here's an example of 25x25 puzzle:
4 2 1 2 2
4 1 1 3
4 2 2 3
8 10
6 3 9
3 1 1 9
2 1 1 8
2 1 1 2 2 5
1 1 4 1 3
2 9 6
13 7
4 1 6 4 2
1 1 3 3 3
1 3 1 1 2
2 8 2
5 1 4 2
5 3 1 2
5 2 4
6 2 3
5 1 2
3 4 2
4 2 3 2
6 3 4 3
8 4 1
1 1 4 4
-
6 1 2
1 5 1 3
6 8 3
5 5 10
5 4 9
4 2 9
1 1 5 1
1 3 1 2 2
4 2 1 2
1 1 6 2
1 3 8
10
5 5 3
9 6
4 5 1 5
6 3 2 5
4 1
8
1 6 2 1
4 5 1
5 5 1 1
7 9 1
11 2 2 3
4 6 6
5 6
Solver
#!/usr/bin/env crystal
require "z3"
class Nonograms
@col_hints : Array(Array(Int32))
@row_hints : Array(Array(Int32))
def initialize(path)
col, row = File.read(path).split("-\n", 2)
@col_hints = col.chomp.split("\n").map{|l| l.split.map(&.to_i)}
@row_hints = row.chomp.split("\n").map{|l| l.split.map(&.to_i)}
@xsize = @col_hints.size
@ysize = @row_hints.size
@solver = Z3::Solver.new
@cells = {} of Tuple(Int32, Int32) => Z3::BoolExpr
end
def column_cells(x)
(0...@ysize).map{|y| @cells[{x,y}]}
end
def row_cells(y)
(0...@xsize).map{|x| @cells[{x,y}]}
end
def setup_groups(name, hints, cells)
count = hints.size
starts = (0...count).map{|i| Z3.int("#{name} start #{i}") }
ends = (0...count).map{|i| Z3.int("#{name} end #{i}") }
# Every group is on the board
count.times do |i|
@solver.assert starts[i] >= 0
@solver.assert ends[i] <= cells.size
end
# Every group has correct size
hints.each_with_index do |hint, i|
@solver.assert starts[i] + hint == ends[i]
end
# There is a gap between groups
(count-1).times do |i|
@solver.assert starts[i+1] >= ends[i] + 1
end
# Each filled cell belongs to one of the groups
cells.each_with_index do |c, j|
cell_j_in_group_i = count.times.map{|i| (j >= starts[i]) & (j < ends[i]) }
# this is fairly awkward and we should probably add Z3.or()
cell_j_in_any_group = count == 0 ? false : cell_j_in_group_i.reduce{|a,b| a|b}
@solver.assert c == cell_j_in_any_group
end
end
def call
# Setup cell variables
@xsize.times do |x|
@ysize.times do |y|
@cells[{x,y}] = Z3.bool("cell #{x},#{y}")
end
end
# Setup groups
@col_hints.each_with_index do |hints, x|
setup_groups("c#{x}", hints, column_cells(x))
end
@row_hints.each_with_index do |hints, y|
setup_groups("r#{y}", hints, row_cells(y))
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
Nonograms.new(ARGV[0]).call
The code is mostly straightforward, however there are some issues:
-
cell_j_in_any_group = count == 0 ? false : cell_j_in_group_i.reduce{|a,b| a|b}calculations is really ugly - we'd much rather see something like@solver.assert c == Z3.or(cell_j_in_group_i)- and same forZ3.and,Z3.mul, andZ3.add - just like with previous solvers,
Z3::Model#[]not guaranteeing return type is a problem, and instead of(model[@cells[{x, y}]].to_s == "true")we'd much rather havemodel[@cells[{x, y}]].to_b- this is not completely straightforward as.to_iwill need to return aBigIntfor Z3 integers and bitvectors (notInt32), and there's no good object to return for Z3 reals.
Result
$ ./nonograms 1.txt
...######......#......##.
#..#####.......#......###
######.....########..###.
#####..#####..##########.
#####....####..#########.
.####.....##....#########
...#......#....#####...#.
...#.....###..#...##..##.
....####.##...#......##..
#...#....######......##..
#...###..########........
.........##########......
.......#####..#####...###
.......#########...######
..####..#####.#.....#####
######..###.##......#####
...####.............#....
########.................
#.######..##....#........
...####.#####...........#
...#####.#####..#.......#
.#######.#########......#
###########...##.##...###
####..######.....######..
.......#####.....######..
Story so far
Coming next
I want to do a few more puzzle game solvers, but first I want to improve Crystal Z3 shard to fix the issues I had so far.
Top comments (0)