DEV Community

Tomasz Wegrzanowski
Tomasz Wegrzanowski

Posted on

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
..###
Enter fullscreen mode Exit fullscreen mode

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###
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

Or vertical:

a <= 1
h <= 1
b + f + i <= 1
c <= 1
d + g <= 1
e <= 1
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

And finally rules for every numbered hint:

e + g = 0
f + c + g = 1
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

And a bit more propagation:

a = 0
b = 0
c = 0
d = 1
e = 0
f = 1
g = 0
h = 1
i = 0
Enter fullscreen mode Exit fullscreen mode

And we can now fill in the board;

...*.
#*1.0
*.###
Enter fullscreen mode Exit fullscreen mode

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.

Top comments (0)