Exercise 18 | RACSO

Exercise _‹18_›:

VERTEX COVER

\leq

SAT

Reduce the VERTEX COVER problem to the SAT problem. These problems are defined as follows:

VERTEX COVER: given a natural $k$ and an undirected graph $G$ , is there a cover for $G$ of size at most $k$ ? In other words, is there a subset $S$ of nodes with size at most $k$ such that each edge of $G$ involves a node from $S$ ?
More formally, this problem can be defined as the following set:
$\{ \langle k,G=\langle V,E\rangle\rangle \mid \exists S\subseteq V: (|S|\leq k\;\wedge\;\forall \{u,v\}\in E: (u\in S\;\vee\;v\in S)) \}$
SAT: given a boolean formula $F$ in conjunctive normal form, is $F$ satisfiable?
More formally, this problem can be defined as the following set:
$\{ F=C_1\wedge\ldots\wedge C_n \mid F\text{ satisfiable} \}$

The input and output of the reduction conform to the following data types:

```
in: struct {
      k: int
      numnodes: int
      edges: array of array [2] of int
      adjacents: array of array of int
      adjacencymatrix: array of array of int
    }
```
The input is a natural number in.k and an undirected graph. The graph is given by means of four different kinds of information: the number of nodes in.numnodes, the list of edges in.edges, for each node the list of its adjacent nodes in.adjacents, and the adjacency matrix in.adjacencymatrix. The nodes are integers between $1$ and in.numnodes, and thus, the $0$ ’th position of in.adjacents does not contain useful data and should be ignored; for any other position $p$ , in.adjacents[p] is the list of nodes adjacent to $p$ . For the same reason, the $0$ ’th row and column of in.adjacencymatrix do not contain useful data and should be ignored; for any other row $r$ and column $c$ , in.adjacencymatrix[r][c] is $0$ when there is no edge between the nodes $r$ and $c$ , and $1$ otherwise.

Note: The input graph has at least one node, no repeated edges, nor self-loop edges, and the value of in.k is at most the number of nodes of the graph.
```
out: array of array of string
```
The output is a list of clauses. A positive literal is represented by a positive number or by a string not starting with «-», a negated literal by a negative number or a string starting with «-».

Note: If the output is an empty formula, it is considered satisfiable. If the formula has any empty clause, it is considered unsatisfiable.

Authors: Carles Creus / Documentation:

Exercise ‹18›:

Exercise _‹18_›: