Exercise 5 | RACSO

Exercise _‹5:

Flow

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

n=m=k=9

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

      ·   ·   ·   ·   ·   ·   1   2   3           ·---·---·   ·---·---·---1   2   3
                                                  |       |   |               |   |
      ·   4   ·   ·   ·   ·   ·   ·   ·           ·   4   ·   ·   ·---·---·---·   ·
                                                  |   |   |   |   |               |
      5   ·   ·   1   ·   ·   ·   ·   ·           5   ·   ·   1   ·   ·---·---·---·
                                                      |   |       |   |
      ·   ·   ·   2   ·   ·   ·   ·   ·           ·---·   ·   2---·   ·   ·---·---·
                                                  |       |           |   |       |
      ·   3   ·   ·   ·   ·   ·   6   ·           ·   3   ·   ·---·---·   ·   6   ·
                                                  |   |   |   |           |   |   |
      ·   ·   ·   ·   7   ·   ·   ·   ·           ·   ·   ·   ·   7---·   ·   ·   ·
                                                  |   |   |   |       |   |   |   |
      ·   ·   ·   ·   ·   ·   8   ·   8           ·   ·   ·   ·---·   ·   8   ·   8
                                                  |   |   |       |   |       |
      ·   ·   ·   5   ·   ·   7   6   9           ·   ·   ·---5   ·   ·---7   6   9
                                                  |   |           |               |
      4   ·   ·   ·   ·   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 (adaptation) / Documentation:

Exercise ‹5:

Exercise _‹5: