## Exercise ‹11›:

Grid exploration
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:
• grid: array of array of int
k: int
s: struct {
r: int
c: int
}

The input has the matrix grid, the maximum number $k$ of cells in the path (counting $s$), and the initial cell $s$. The grid contains the locations of the walls: grid[i][j] has a $0$ to denote that cell $(i,j)$ is walkable, and a $1$ to denote that the cell has a wall. The starting cell $s$ is a struct with two fields: r indicates the row, and c indicates the column. For instance, in the previous example we would have s.r${} = {}$s.c${} = 4$. It is guaranteed that every walkable cell is reachable from the cell $s$.
• path: array of struct {
r: int
c: int
}

The output consists of an array of variable length, containing the sequence of cells that form the path. Each element in the path is a struct with a pair of numbers r and c, with the same meaning as in s. The $0$’th element of the array must be s.
Authors: Nil Mamano / Documentation:
 reduction { // Write here your reduction to SAT... } reconstruction { // Write here your solution reconstruction... } To be able to submit you need to either log in, register, or become a guest.