Exercise 2 | RACSO

Exercise _‹2_›:

SAT

\leq

DOMINATING SET

Reduce the SAT problem to the DOMINATING SET problem. These problems are defined as follows:

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} \}$
DOMINATING SET: given a natural $k$ and an undirected graph $G$ , is there a subset $S$ of size at most $k$ of nodes that dominates $G$ ? In other words, is there a subset $S$ of nodes with size at most $k$ such that any node of $G$ is either in $S$ or adjacent to a node in $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\in V: (u\in S\;\vee\;\exists v\in S: \{u,v\}\in E)) \}$

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

```
in: struct {
      numvars: int
      clauses: array of array of int
    }
```
The input is a boolean formula in conjunctive normal form: in.numvars specifies the number of variables occurring in the formula, and in.clauses is the list of clauses. Each clause is a list of literals, and each literal is a positive or negative integer: a positive integer $x$ represents the $x$ ’th variable, and a negative integer $-x$ represents the negation of the $x$ ’th variable. Such an $x$ takes values between $1$ and in.numvars.

Note: The input has at least one clause, every clause has at least one literal, and there are no repeated literals in a clause. Thus, in.numvars is at least $1$ .
```
out: struct {
       k: int
       edges: array of array [2] of string
       nodes: array of string
     }
```
The output is a natural number out.k and an undirected graph, which is described with the list of edges out.edges and with the list of nodes out.nodes. An edge is a pair of nodes, and each node is represented by either an integer or a string. The list of nodes out.nodes is optional, and contains nodes of the graph, that may or may not appear in the list of edges. This list of nodes could be useful, for example, for including the nodes that are not connected to any other node, if this is considered necessary.

Note: If the output out.k is negative, then no such dominating set exists. Repeated edges and self-loop edges are ignored.

Authors: Carles Creus, Pau Fernández, Guillem Godoy / Documentation: