## 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:
 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.