Exercise 2 | RACSO

Exercise _‹2_›:

Surrounding numbers

Solve the following exercise by means of a reduction to SAT:

Given an

n\times m

board such that some of the cells contain a number in

\{0,\ldots,3\}

, find a way to draw a set of cycles such that, given a cell with a number

k

, exactly

k

of its four sides are part of a cycle. Cycles can’t share sides nor vertices. The sides of a cell can belong to different cycles.

For example, the following figure represents an input for this problem with

n=m=7

(empty cells are denoted with a dot):

      ·   ·   ·   ·   2   ·   ·

      ·   ·   ·   ·   ·   ·   3

      ·   2   1   ·   ·   ·   ·

      ·   ·   ·   ·   ·   1   0

      0   ·   ·   ·   ·   ·   ·

      ·   ·   ·   ·   ·   3   ·

      ·   ·   ·   ·   3   ·   ·

and this represents a possible solution for it with two cycles:

                        ┌───┐
      ·   ·   ·   ·   2 │ · │ ·
                    ┌───┘   └───┐
      ·   ·   ·   · │ ·   ·   3 │
        ┌───────────┘       ┌───┘
      · │ 2   1   ·   ·   · │ ·
        │           ┌───────┘
      · │ ·   ·   · │ ·   1   0
        └───────────┘
      0   ·   ·   ·   ·   ·   ·
                        ┌───┐
      ·   ·   ·   ·   · │ 3 │ ·
                    ┌───┘   └───┐
      ·   ·   ·   · │ 3   ·   · │
                    └───────────┘

The input of the exercise and the output with the solution (when the input is solvable) are as follows:

```
board: array of array of int
```
The input is an $n\times m$ matrix. Each of its cells either has a value in $\{0,\ldots,3\}$ , or it has the value $-1$ to denote that the cell is empty.
```
segments: array of array [2] of struct {
   r: int
   c: int
}
```
The output is a list of pairs of adjacent cells. Each cell is identified with its coordinates r (row) and c (column). Each of the pairs of adjacent cells denotes that the segment adjacent to both cells is part of a cycle.

Note that in some cases it will be necessary to identify cells that are outside the board (see, e.g., the small cycle surrounding two $3$ -cells in the example, which involves four segments that separate a cell from the void outside the board). For this reason, the value of r can be any number in $\{-1,\ldots,n\}$ instead of $\{0,\ldots,n-1\}$ , and the value of c any number in $\{-1,\ldots,m\}$ instead of $\{0,\ldots,m-1\}$ : this allows to identify one extra cell around the whole board.

Authors: Carles Creus, Nil Mamano (adapted from the exercises of the Logic in Information Technology subject) / Documentation:

Exercise ‹2›:

Exercise _‹2_›: