Open Source Adventures: Episode 73: How to solve Light Up Puzzle with math

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.

In the followup post I'll show to do write a Crystal Z3 solver for it. But this time, instead of going straight to the code, let's try to write some rules by hand.

Writing equations by hand

Let's say this is tiny board:

.....
#.1.0
..###

We need variables for every empty slot. In the solver we could also have equations for wall cells (forced to equal 0) for sake of code simplicity, and it really makes no difference to Z3 engine. So cell variables are a to i. Z3 distinguishes integers from booleans so we'll need to do some casts in real code, but to keep things simple I'll just treat false as 0 and true as 1 here.

abcde
#f1g0
hi###

So first thing we need to do is create groups, here are horizontal groups:

• a, b, c, d, e
• f
• g
• h, i

And here are vertical groups:

• a
• h
• b, f, i
• c
• d, g
• e

Let's name them after their first element. So ah is horizontal group starting with a, av is vertical group starting with a.

Now it's time to write equations. First, no group can have more than one active element, horizontal:

a + b + c + d + e <= 1
f <= 1
g <= 1
h + i <= 1

Or vertical:

a <= 1
h <= 1
b + f + i <= 1
c <= 1
d + g <= 1
e <= 1

Now let's define group variables. We can use either + or | on the right side, as they're all either 0 or 1 (due to previous rule):

ah = a | b | c | d | e
fh = f
gh = g
hh = h | i

av = a
hv = h
bv = b | f | i
cv = c
dv = d | g
ev = e

By rules every cell needs a light in either its horizontal or vertical group:

ah | av = 1 # a
ah | bv = 1 # b
ah | cv = 1 # c
ah | dv = 1 # d
ah | ev = 1 # e
fh | bv = 1 # f
gh | dv = 1 # g
hh | hv = 1 # h
hh | bv = 1 # i

And finally rules for every numbered hint:

e + g = 0
f + c + g = 1

Solve this system of equations by hand

We ended up with the following system of 31 equations:

a + b + c + d + e <= 1
f <= 1
g <= 1
h + i <= 1
a <= 1
h <= 1
b + f + i <= 1
c <= 1
d + g <= 1
e <= 1
ah = a | b | c | d | e
fh = f
gh = g
hh = h | i
av = a
hv = h
bv = b | f | i
cv = c
dv = d | g
ev = e
ah | av = 1
ah | bv = 1
ah | cv = 1
ah | dv = 1
ah | ev = 1
fh | bv = 1
gh | dv = 1
hh | hv = 1
hh | bv = 1
e + g = 0
f + c + g = 1

We can start by replacing all the single-element variables, removing all single variable <= 1 constraints as always true, and splitting e + g = 0 into e = 0 and g = 0.

a + b + c + d + e <= 1
h + i <= 1
b + f + i <= 1
d + g <= 1
ah = a | b | c | d | e
hh = h | i
bv = b | f | i
dv = d | g
ah | a = 1
ah | bv = 1
ah | c = 1
ah | dv = 1
ah | e = 1
f | bv = 1
g | dv = 1
hh | h = 1
hh | bv = 1
e = 0
g = 0
f + c + g = 1

We already have two knowns (e and g), let's propagate those zeroes:

e = 0
g = 0

a + b + c + d + 0 <= 1
h + i <= 1
b + f + i <= 1
d + 0 <= 1
ah = a | b | c | d | 0
hh = h | i
bv = b | f | i
dv = d | 0
ah | a = 1
ah | bv = 1
ah | c = 1
ah | dv = 1
ah | 0 = 1
f | bv = 1
0 | dv = 1
hh | h = 1
hh | bv = 1
f + c + 0 = 1

We can simplify x | 0 and x + 0 to x, and drop redundant d + 0 <= 1:

e = 0
g = 0

a + b + c + d <= 1
h + i <= 1
b + f + i <= 1
ah = a | b | c | d
hh = h | i
bv = b | f | i
dv = d
ah | a = 1
ah | bv = 1
ah | c = 1
ah | dv = 1
ah = 1
f | bv = 1
dv = 1
hh | h = 1
hh | bv = 1
f + c = 1

Now we can propagate dv and ah:

d = 1
e = 0
g = 0

a + b + c + d <= 1
h + i <= 1
b + f + i <= 1
1 = a | b | c | d
hh = h | i
bv = b | f | i
1 | a = 1
1 | bv = 1
1 | c = 1
1 | d = 1
f | bv = 1
hh | h = 1
hh | bv = 1
f + c = 1

We can replace all 1 | x by 1, and that just results in a bunch of 1 = 1 we can drop:

d = 1
e = 0
g = 0

a + b + c + 1 <= 1
h + i <= 1
b + f + i <= 1
hh = h | i
bv = b | f | i
hh | h = 1
hh | bv = 1
f + c = 1

a + b + c + 1 <= 1 means a + b + c must all equal 0, so we have three more variables:

a = 0
b = 0
c = 0
d = 1
e = 0
g = 0

h + i <= 1
0 + f + i <= 1
hh = h | i
bv = 0 | f | i
hh | h = 1
hh | bv = 1
f + 0 = 1

This gives us f:

a = 0
b = 0
c = 0
d = 1
e = 0
f = 1
g = 0

h + i <= 1
1 + i <= 1
hh = h | i
bv = 1
hh | h = 1
hh | bv = 1

From 1 + i <= 1 we know i = 1, we can also propagate bv:

a = 0
b = 0
c = 0
d = 1
e = 0
f = 1
g = 0
i = 0

h + 0 <= 1
hh = h | 0
hh | h = 1
hh | 1 = 1

And a bit more propagation:

a = 0
b = 0
c = 0
d = 1
e = 0
f = 1
g = 0
h = 1
i = 0

And we can now fill in the board;

...*.
#*1.0
*.###

As you can see, it fulfills all the rules.

On a bigger board, solving it would be harder. But it's just as easy to create similar system of equations no matter board size, and let Z3 engine solve them.

That's pretty much what Z3 programming is about. You don't need to be able to solve the equations, but you need to be able to write them down. Then Z3 engine handles the rest.

Story so far

All the code is on GitHub.

Coming next

In the next episode I'll show Crystal Z3 code for this solver, then it will be time to move on to different projects.