Open Source Adventures: Episode 64: How to write Z3 Solvers for Puzzle Games?

Z3 has many uses, but a good fun use is solving puzzle games!

Puzzle Team created a lot of nice online puzzles. They weirdly don't have one domain, and use a different domain for each puzzle. Maybe that's some advanced SEO trick.

So let's go through some of the puzzles, covering:

• what is the puzzle
• what are the constraints
• how difficult it is for Z3
• primary variables (the ones that will become part of the solution)
• any auxiliary variables
• how to approach writing a solver

There won't be any code in this episode, but I'll do a few of them in future episodes. Here's just some draft to give you an idea what Z3 is good at, and what it's not so good at.

Mosaic

Puzzle is NxM grid, every cell has is White or Black.

Some cells also have number in them (0-9). Any such cell must have exactly that many Black cells in its neighborhood (itself plus any touching cells).

This is a trivial one to write solver for.

Primary variables are NxM booleans. White for false, Black for true, or the other way.

For every constrained cell, we just need to tell the solver how many variables around it are true.

Alternatively we could use numbers 0 or 1 instead of booleans, because we're adding them. It shouldn't make much difference.

Minesweeper

Puzzle is NxM grid, every cell has is Mine or Empty.

Some cells also have number in them (0-8). Any such cell must have exactly that many Mine cells in its neighborhood, excluding itself.

This is a trivial one to write solver for.

It's literally Mosaic puzzle, except here clue cells are always Empty.

Slant

Puzzle is NxM grid, every cell has Forward Diagonal or Backward Diagonal.

Some intersections have numbers (0-4). Any such intersection must have that many diagonals touching it.

Diagonals are not allowed to create loops.

This is a bit tricky to write solver for.

For primary variables, every cell can be a boolean. Or pair of booleans (is Forward Diagonal, is Backward Diagonal) that are always opposite of each other, just to make things simpler later.

The intersection condition is very simple.

The no-loops condition is pretty much impossible to code as-is, we cannot list every possible loop, and there's exponentially many of them. We'd need to find alternative rule that is easier to code that is equivalent.

I think the most obvious equivalent rule is that every intersection is connected to the edge through diagonals (I think that's equivalent). In such case we'd need auxiliary variable for every intersection "distance to edge". Every intersection on edge would have its number set to 0. Every one not on the edge would have its number set to 1 plus minimum of distances of its connected intersections.

LITS

Puzzle is NxM grid divided into irregularly shaped areas. Every cell is Filled or Empty.

Rules are:

• in every area there's exactly 4 Filled cells, making one of tetrominos I, L, S, or T (J = L, and Z = S)
• no 2x2 area can be all Filled
• no tetromino can border another tetromino of the same type
• all cells are connected

This puzzle is quite difficult to write solver for.

Primary variables Fxy are NxM booleans. Filled for true, Empty for false.

But we'd need a lot of auxiliary variables to make it work. One approach would be to have:

• auxiliary variable Ais (I, L, S, or T) for every area indicating its shape
• auxiliary variable Cij for every pair of neighbouring shapes if they're connected by Filled cells or not
• auxiliary variable Di for distance from the first area

The "no 2x2 area is all Filled" rule is trivial, no Fxy Fx(y+1) F(x+1)y F(x+1)(y+1) can all be filled.

For every area and every shape, we'd need to create a rule listing all its possible placements, so let's say A1I would mean one of (F11, F12, F13, F14, not F15) or (not F11, F12, F13, F14, F15).

Then we'd need a rule defining Cij based on all bordering Fxy of both areas.

Then we'd define that if Cij is true, then AiL and AjL can't both be true, and so on for every pair of areas, and every shape.

And finally we'd need to define Di as 0 for first area, and 1 + minimum of connected Djs for every other area, to make sure everything is connected.

Galaxies

Puzzle is NxM grid you need to divide into "galaxies". There are some number of points (on centers, intersections, or edges of cells) marked as centers of galaxies. Each galaxy has rotational symmetry.

This puzzle has an obvious partial solver, and a bit tricker full solver.

If there's G galaxies, we can number the centers 1 to G. Then primary variables Cxy can be NxM integers from 1 to G, if a cell belongs to given galaxy.

For every cell xy and every galaxy g, we can define that Cxy == g only if Cwz == g, where wz is xy rotated around center of g. If that center is outside the grid, then Cxy != g.

This isn't quite a full solver, as "regions" it generates can in principle be non-contiguous. That could be seen with this puzzle:

|---|---|---|---|---|---|---|---|---|---|---|---|
|   |   |   |   |   |   |   |   |   |   |   |   |
|---|---O---|---|---|---O---|---|---|---O---|---|
|   |   |   |   |   |   |   |   |   |   |   |   |
|---|---|---|---|---|---|---|---|---|---|---|---|

This has correct solution:

|---|---|---|---|---|---|---|---|---|---|---|---|
| 1 | 1 | 1 | 1 | 2 | 2 | 2 | 2 | 3 | 3 | 3 | 3 |
|---|---O---|---|---|---O---|---|---|---O---|---|
| 1 | 1 | 1 | 1 | 2 | 2 | 2 | 2 | 3 | 3 | 3 | 3 |
|---|---|---|---|---|---|---|---|---|---|---|---|

But our partial solver could also come up with this:

|---|---|---|---|---|---|---|---|---|---|---|---|
| 2 | 1 | 1 | 2 | 2 | 2 | 2 | 2 | 2 | 3 | 3 | 2 |
|---|---O---|---|---|---O---|---|---|---O---|---|
| 2 | 1 | 1 | 2 | 2 | 2 | 2 | 2 | 2 | 3 | 3 | 2 |
|---|---|---|---|---|---|---|---|---|---|---|---|

So we also need to give every cell an auxiliary variable "distance", measured from the center of that cell's galaxy, to make sure it's actually connected.

Sudoku

Puzzle is a 9x9 grid, with numbers (1-9) in each cell. Every row, column, and 3x3 block must contain all numbers from 1 to 9.

This is a super easy. Primary variables are 9x9 integers from 1 to 9. Z3 has a "everything in this set is distinct" constraint, so we can use it instead of a lot of "not equals" constraints.

And so many other puzzles

When writing solvers for puzzle games:

• you need to decide what are the primary variables
• "local" constraints, that depend only on a few primary variables, are very easy, and Z3 can deal with them in a highly performant way
• "global" constraints, that depend on many or all primary variables, are very hard. Constraints like "everything is one loop", "everything is connected", "there are no loops" etc. usually cause a lot of trouble. You'll likely need to rewrite the rules, introduce some auxiliary variables - and depending on how you do this, this can cause very poor performance

Coming next

Over the next few episodes I'll write a few Z3 solvers for puzzle games, and do some detailed explanations of how to do them.