Solve the following exercise by means of a reduction to
SAT:
- Given a grid made of walkable cells and walls,
and a walkable cell s, find a path from s and through adjacent
cells such that every walkable cell is visited at least once.
The path must not contain more than k cells.
The ending point of the path does not matter.
For instance, for the grid
· # · # #
· · · · ·
· # · # ·
· · · · ·
# # · # s
in which walls have been indicated with a #, the following path
1) 2) 3)
· # · # # · # · # # · # · # #
^
· · · · · · · · · · · · · · ·
^
· # · # · · # · # · · # o # ·
^ ^ v
· · · < · < · · · o o o · < · < o o o
v ^ ^
# # · # s # # o # o # # o # o
4) 5) 6)
o # · # # o # o # # o # o # #
v ^ v
o > · > · · · o o o > · > · o o o o o
v
o # o # · o # o # · o # o # o
o o o o o o o o o o o o o o o
# # o # o # # o # o # # o # o
visits all walkable cells, and has 21 cells (note that the initial s in the
path is also counted).
The input of the exercise and the output with the solution (when the input is
solvable) are as follows: