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 figures represent an input for this problem with

n=m=7

and a possible solution with two cycles:

    +---+---+---+---+---+---+---+         +---+---+---+---+---╔═══╗---+
    ¦   ¦   ¦   ¦   ¦ 2 ¦   ¦   ¦         ¦   ¦   ¦   ¦   ¦ 2 ║   ║   ¦
    +---+---+---+---+---+---+---+         +---+---+---+---╔═══╝---╚═══╗
    ¦   ¦   ¦   ¦   ¦   ¦   ¦ 3 ¦         ¦   ¦   ¦   ¦   ║   ¦   ¦ 3 ║
    +---+---+---+---+---+---+---+         +---╔═══════════╝---+---╔═══╝
    ¦   ¦ 2 ¦ 1 ¦   ¦   ¦   ¦   ¦         ¦   ║ 2 ¦ 1 ¦   ¦   ¦   ║   ¦
    +---+---+---+---+---+---+---+         +---║---+---+---╔═══════╝---+
    ¦   ¦   ¦   ¦   ¦   ¦ 1 ¦ 0 ¦         ¦   ║   ¦   ¦   ║   ¦ 1 ¦ 0 ¦
    +---+---+---+---+---+---+---+         +---╚═══════════╝---+---+---+
    ¦ 0 ¦   ¦   ¦   ¦   ¦   ¦   ¦         ¦ 0 ¦   ¦   ¦   ¦   ¦   ¦   ¦
    +---+---+---+---+---+---+---+         +---+---+---+---+---╔═══╗---+
    ¦   ¦   ¦   ¦   ¦   ¦ 3 ¦   ¦         ¦   ¦   ¦   ¦   ¦   ║ 3 ║   ¦
    +---+---+---+---+---+---+---+         +---+---+---+---╔═══╝---╚═══╗
    ¦   ¦   ¦   ¦   ¦ 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_›: