Exercise ‹2›:

Surrounding numbers
Note: this problem has been taken from the Logic in Information Technology subject at Barcelona School of Informatics.

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 (adaptation) / 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.