Modelling and solving the "Light Up" decision puzzle

In this tutorial, you'll model and solve the "Light Up" decision puzzle using Paramita. Along the way, you'll learn how to create Boolean variables, build logical expressions, convert them to CNF, and solve the resulting SAT instance.

The Light Up puzzle

"Light Up" is a puzzle where you try to place light bulbs in a grid in a way that they light up all the blank squares. In this puzzle, a bulb lights up all the squares in the same row and column up to a wall. The restriction is that some walls have numbers, and we must place that amount of lights orthogonally (in blank spaces) to the wall, and that a bulb cannot light another bulb.

Light Up Example	Solution (white circles are the bulbs).

You can play the puzzle from the puzzle collection created by Simon Tatham here

Light Up is an NP-Complete problem¹.

Modelling the problem

Let's define our puzzle first.

We define the problem:

from itertools import product

nrows, ncols = (7, 7)

cells = [
    [' ',' ',' ','0',' ',' ',' '],
    [' ',' ',' ',' ','1',' ',' '],
    [' ','2',' ',' ',' ',' ',' '],
    ['3',' ',' ',' ',' ',' ','W'],
    [' ',' ',' ',' ',' ','2',' '],
    [' ',' ','W',' ',' ',' ',' '],
    [' ',' ',' ','2',' ',' ',' '],
]

blank_cells = {
    (r,c)
    for (r,c) in product(range(nrows), range(ncols))
    if cells[r][c] == ' '
}
numbered_cells = {
    (r,c): int(cells[r][c])
    for (r,c) in product(range(nrows), range(ncols))
    if cells[r][c] != ' ' and cells[r][c] != 'W'
}

For each cell in the grid, we define a Boolean variable that is true iff the cell has a bulb. In Paramita, we create Boolean variables using the Bool class. Each variable needs a unique name:

from paramita.modelling import Bool

def bulb(r,c):
    return Bool(f"bulb_{r}_{c}")

If you create two Bools with the same name, they will be treated as the same variable. This is useful when you need to refer to the same variable from different parts of your code.

Now, for the first constraint:

A numbered wall must have exactly that amount of bulbs in orthogonal blank cells.

We can define a function that yields the orthogonal blank neighbours of a cell:

def orthogonal(r,c):
    if r > 0 and (r-1,c) in blank_cells:
        yield (r-1, c)
    if c > 0 and (r,c-1) in blank_cells:
        yield (r, c-1)
    if r < nrows - 1  and (r+1,c) in blank_cells:
        yield(r+1, c)
    if c < ncols - 1  and (r,c+1) in blank_cells:
        yield(r, c+1)

Then for each numbered cell, we collect the bulb variables in the orthogonal positions and constrain their sum to equal the number:

constraints = []
for cell, number in numbered_cells.items():
    orth = [bulb(r,c) for (r,c) in orthogonal(*cell)]
    constraints.append(sum(orth) == number)

These type of constraints are called "Pseudo-Boolean" (PB) expressions.

The second constraint is:

Each blank cell is lit by at least one bulb. A bulb lights all cells in the same row and column until a wall (a numbered cell or the grid edge).

So first we need a function that yields all cells visible from a given blank cell, including itself:

DIRECTIONS = [(-1, 0), (1, 0), (0, -1), (0, 1)]

def visible_cells(r, c):
    yield (r, c)
    for dr, dc in DIRECTIONS:
        r2, c2 = r + dr, c + dc
        while (r2, c2) in blank_cells:
            yield (r2, c2)
            r2 += dr
            c2 += dc

Now, for each blank cell, the sum of bulbs in its visible cells must be at least one:

for (r,c) in blank_cells:
    visible = visible_cells(r, c)
    constraints.append(
        sum(bulb(*c) for c in visible) >= 1
    )

Again, we are using PB expressions to specify these constraints.

The last constraint is:

A bulb cannot lit another bulb.

If a blank cell has a bulb, then among all cells visible from it (including itself), there must be exactly one bulb: itself.

from paramita.modelling import If
for (r,c) in blank_cells:
    visible = visible_cells(r, c)
    constraints.append(If(
        bulb(r, c),
        sum(bulb(*c) for c in visible) == 1
    ))

Finally, we specify that all the constraints must hold by using the And operator:

from functools import reduce
from paramita.modelling import And
expr = reduce(And, constraints)

In this example, we are using the functools.reduce function to apply the And operator (which is a binary operator) to all the constraints.

Solving the problem

Prerequisites

You need a SAT solver compiled as a Paramita extension. Start by fetching Cadical 3.0.0 from the Paramita Plugins repository using the CLI helper:

paramita plugins build cmake "#sat-solvers/cadical-3.0.0"

For more information you can check the Building an external Plugin section.

At this point, we can send all the constraints to a SAT solver, and ask for a solution:

from paramita.solvers import SatSolver
from paramita.modelling import DimacsVariablePool, add_to_container, to_cnf
s = SatSolver.from_name("Cadical300")
pool = DimacsVariablePool()
add_to_container(expr, to_cnf, s, pool)

Let's break down what each line does:

1. s = SatSolver.from_name("Cadical300") creates an instance of the Cadical300 SAT solver that we previously compiled and installed following the instructions in the Building an external Plugin.
2. pool = DimacsVariablePool() keeps track of the mapping between our variable names (like "x") and the numbers that DIMACS CNF format requires. The first variable gets number 1, the second gets 2, and so on.
3. add_to_container(expr, to_cnf, s, pool) does the actual work: it converts expr to CNF using to_cnf, then adds all the resulting clauses to the SAT solver s, using pool to assign numbers to variable names. Notice that to_cnf is a function that takes an expression and converts it to CNF. Paramita provides this conversion for you.

Note

We can directly use a SatSolver because add_to_container expects a ClauseContainer, which conviniently SatSolver subclasses from.

Finally, we can solve the problem and retrieve the solution:

s.solve()

m = s.model()

for lit in m:
    if lit > 0:
        var = pool.decode_literal(lit).name
        if var.startswith("bulb_"):
            _, r,c = var.split("_")
            print(f"{r},{c} has a bulb")

We use the pool.decode_literal(...) function to convert from the SAT solver's variable identifiers to our identifiers containing the coordinates where bulbs are placed.

Alternatives to storing constraints in a list

Alternatively to having a list of constraints, we could have had constructed the expression along the way, by doing something like:

expr = True
for cell, number in numbered_cells.items():
    orth = [bulb(r,c) for (r,c) in orthogonal(*cell)]
    expr = expr & (sum(orth) == number)

Or even add the constraints to the container directly:

s = SatSolver....()
pool = DimacsVariablePool()

for cell, number in numbered_cells.items():
    orth = [bulb(r,c) for (r,c) in orthogonal(*cell)]
    e = sum(orth)==number
    add_to_container(e, to_cnf, s, pool)

Source code

This is the source code for the full example:

from itertools import product

nrows, ncols = (7, 7)

cells = [
    [' ',' ',' ','0',' ',' ',' '],
    [' ',' ',' ',' ','1',' ',' '],
    [' ','2',' ',' ',' ',' ',' '],
    ['3',' ',' ',' ',' ',' ','W'],
    [' ',' ',' ',' ',' ','2',' '],
    [' ',' ','W',' ',' ',' ',' '],
    [' ',' ',' ','2',' ',' ',' '],
]

blank_cells = {
    (r,c)
    for (r,c) in product(range(nrows), range(ncols))
    if cells[r][c] == ' '
}
numbered_cells = {
    (r,c): int(cells[r][c])
    for (r,c) in product(range(nrows), range(ncols))
    if cells[r][c] != ' ' and cells[r][c] != 'W'
}

from paramita.modelling import Bool

def bulb(r,c):
    return Bool(f"bulb_{r}_{c}")

def orthogonal(r,c):
    if r > 0 and (r-1,c) in blank_cells:
        yield (r-1, c)
    if c > 0 and (r,c-1) in blank_cells:
        yield (r, c-1)
    if r < nrows - 1  and (r+1,c) in blank_cells:
        yield(r+1, c)
    if c < ncols - 1  and (r,c+1) in blank_cells:
        yield(r, c+1)

constraints = []
for cell, number in numbered_cells.items():
    orth = [bulb(r,c) for (r,c) in orthogonal(*cell)]
    constraints.append(sum(orth) == number)

DIRECTIONS = [(-1, 0), (1, 0), (0, -1), (0, 1)]

def visible_cells(r, c):
    yield (r, c)
    for dr, dc in DIRECTIONS:
        r2, c2 = r + dr, c + dc
        while (r2, c2) in blank_cells:
            yield (r2, c2)
            r2 += dr
            c2 += dc

for (r,c) in blank_cells:
    visible = visible_cells(r, c)
    constraints.append(
        sum(bulb(*c) for c in visible) >= 1
    )

from paramita.modelling import If
for (r,c) in blank_cells:
    visible = visible_cells(r, c)
    constraints.append(If(
        bulb(r, c),
        sum(bulb(*c) for c in visible) == 1
    ))

from functools import reduce
from paramita.modelling import And
expr = reduce(And, constraints)

from paramita.solvers import SatSolver
from paramita.modelling import DimacsVariablePool, add_to_container, to_cnf
s = SatSolver.from_name("Cadical300")
pool = DimacsVariablePool()
add_to_container(expr, to_cnf, s, pool)

s.solve()

m = s.model()

for lit in m:
    if lit > 0:
        var = pool.decode_literal(lit).name
        if var.startswith("bulb_"):
            _, r,c = var.split("_")
            print(f"{r},{c} has a bulb")

---

1. Brandon McPhail. Light up is np-complete. Unpublished manuscript, 2005. ↩