Exercise 5 | RACSO

Exercise _‹5:

Flow

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

Given an

n\times m

board and

2k

pipe ends (

k

pairs, with a different color for each pair) in certain positions of the board, determine if the pipe ends of matching colors can be connected with pipes through the board in a way that no pipes overlap and the whole board is covered.

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

n=m=k=9

(numbers identify the pipe ends with matching colors, empty cells are denoted with a dot):

      ·   ·   ·   ·   ·   ·   1   2   3

      ·   4   ·   ·   ·   ·   ·   ·   ·

      5   ·   ·   1   ·   ·   ·   ·   ·

      ·   ·   ·   2   ·   ·   ·   ·   ·

      ·   3   ·   ·   ·   ·   ·   6   ·

      ·   ·   ·   ·   7   ·   ·   ·   ·

      ·   ·   ·   ·   ·   ·   8   ·   8

      ·   ·   ·   5   ·   ·   7   6   9

      4   ·   ·   ·   ·   9   ·   ·   ·

and this represents be a possible solution for it:

      ·───·───·   ·───·───·───1   2   3
      │       │   │               │   │
      ·   4   ·   ·   ·───·───·───·   ·
      │   │   │   │   │               │
      5   ·   ·   1   ·   ·───·───·───·
          │   │       │   │
      ·───·   ·   2───·   ·   ·───·───·
      │       │           │   │       │
      ·   3   ·   ·───·───·   ·   6   ·
      │   │   │   │           │   │   │
      ·   ·   ·   ·   7───·   ·   ·   ·
      │   │   │   │       │   │   │   │
      ·   ·   ·   ·───·   ·   8   ·   8
      │   │   │       │   │       │
      ·   ·   ·───5   ·   ·───7   6   9
      │   │           │               │
      4   ·───·───·───·   9───·───·───·

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
k: int
```
The input is the $n\times m$ matrix board, and the number $k$ of pipe end pairs. A cell board[i][j] contains a $0$ when it is empty, and a number $p\in\{1,\ldots,k\}$ when it contains one of the pipe ends for the pair $p$ .
```
segments: array of array [2] of struct {
   r: int
   c: int
}
```
The output is a list of cell pairs, each cell being identified by a struct with the fields r (row) and c (column). Each pair of cells denotes that there is a pipe segment connecting those two cells, which must be adjacent cells.

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

Exercise ‹5:

Exercise _‹5: