Z3 is quite amazing, and whenever I show it to people on various unconferences response is very enthusiastic, but it desperately needs some tutorials.

I wrote one for sudoku, but sudoku is maybe just a too straightforward example - variables are simply what goes into cells, and constraints are simply game rules. Usually you'll need at least *a bit* more modelling than that.

So let's try something just a bit more complicated - nonograms:

Nonograms are a puzzle where there's a grid of cells, either filed or empty.

Every row and column has numbers describing cells as seen from its own perspective. So if a row has numbers "2 7" next to it, it means there's a group of 2 filled cells, and then (with at least one empty cell gap) another group of 7 filled cells.

I'm going to refer to both rows and columns as "stripes", as logic for both is exactly the same, so it's simpler to just write it once.

### Get the data

So the first thing we do is OCR that image... Just kidding, we'll transcribe it manually, as setting up proper OCR would take longer than that.Of course in a real solver these numbers would come from somewhere - probably an HTML scrapper, but it could really be OCR, or something else altogether.

```
class NonogramSolver
def initialize
@row_constraints = [
[3],
[5],
[3,1],
[2,1],
[3,3,4],
[2,2,7],
[6,1,1],
[4,2,2],
[1,1],
[3,1],
[6],
[2,7],
[6,3,1],
[1,2,2,1,1],
[4,1,1,3],
[4,2,2],
[3,3,1],
[3,3],
[3],
[2,1],
]
@column_constraints = [
[2],
[1,2],
[2,3],
[2,3],
[3,1,1],
[2,1,1],
[1,1,1,2,2],
[1,1,3,1,3],
[2,6,4],
[3,3,9,1],
[5,3,2],
[3,1,2,2],
[2,1,7],
[3,3,2],
[2,4],
[2,1,2],
[2,2,1],
[2,2],
[1],
[1],
]
@row_count = @row_constraints.size
@column_count = @column_constraints.size
@solver = Z3::Solver.new
end
end
```

### Setting up cell variables

Z3 variables are basically just Symbols with types, and Z3's boolean sort already has the right range, so we don't need to do anything special. A helper functionFor convenience let's write helpers to return row and column of such variables.

None of these functions are strictly necessary and it's totally reasonable to do such calculations where they're needed.

```
def cell(x,y)
Z3.Bool("cell#{x},#{y}")
end
def row(y)
(0...@column_count).map{|x| cell(x,y) }
end
def column(x)
(0...@row_count).map{|y| cell(x,y) }
end
```

### Express grid constraints as stripe constraints

Every stripe (row or column) is independent, so let's write our grid constraints in terms of constraints over individual stripes.We're passing unique identifier like

`"row-4"`or

`column-7`to the following function, as they'll need to setup some variables, which need to be unique, and such meaningful names make debugging easier than just allocating variable names at random.

```
def setup_grid_constraints!
(0...@column_count).each do |x|
setup_stripe_constraints! "column-#{x}", @column_constraints[x], column(x)
end
(0...@row_count).each do |y|
setup_stripe_constraints! "row-#{y}", @row_constraints[y], row(y)
end
end
```

### Constraints for single stripe

Everything we've written so far was trivial, but here comes some real modelling. We have match group size constraints - an array like`[4,2,2]`with an array of boolean cell variables.

How would we model that? Here's one idea:

- For every group have its starting and ending cell as integer variable
- All starts and ends must fit within stripe size - between 0 and N-1 for stripe with N cells
- Difference between start and end equals group size minus one
- Difference between end of one group and start of the next is at least 2
- Cell is filled (true) if and only if it's between start and end of one of the groups

```
def setup_stripe_constraints!(stripe_name, stripe_constraints, stripe)
group_count = stripe_constraints.size
group_start = (0...group_count).map{|i| Z3.Int("#{stripe_name}-#{i}-start")}
group_end = (0...group_count).map{|i| Z3.Int("#{stripe_name}-#{i}-end")}
# Start and end of each group
(0...group_count).each do |i|
@solver.assert (group_start[i] >= 0) & (group_start[i] < stripe.size)
@solver.assert (group_end[i] >= 0) & (group_end[i] < stripe.size)
@solver.assert group_end[i] - group_start[i] == stripe_constraints[i] - 1
end
# Gap between each group and following group
(0...group_count).each_cons(2) do |i,j|
@solver.assert group_start[j] >= group_end[i] + 2
end
# Cells
(0...stripe.size).each do |k|
cell_in_specific_group = (0...group_count).map{|i|
(k >= group_start[i]) & (k <= group_end[i])
}
@solver.assert stripe[k] == Z3.Or(*cell_in_specific_group)
end
end
```

### Print the result

And that's it. Let's print the results, and while at it, why not use some Unicode to spice them up```
def solve!
setup_grid_constraints!
if @solver.satisfiable?
model = @solver.model
(0...@row_count).each do |y|
(0...@column_count).each do |x|
value = model[cell(x,y)].to_s
print value == "true" ? "\u25FC" : "\u25FB"
end
print "\n"
end
else
puts "Nonogram has no solution"
end
end
```

### Results

Just as expected.

### Next Steps

I'd strongly recommend everyone to play with Z3. Logic puzzles are definitely not its main application, they're just great for showing basic techniques without getting bogged down with details of real world problems.The gem itself contains a collection of examples and you're definitely welcome to contribute more.

If posts like this one are popular, I can keep writing tutorials more increasingly more complex and realistic problems.

## No comments:

Post a Comment