Exercise 5 | RACSO

Exercise _‹5_›:

SAT

\leq

CLIQUE

Reduce the SAT problem to the CLIQUE 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} \}$
CLIQUE: given a natural $k$ and an undirected graph $G$ , is there a subset $S$ of nodes with size at least $k$ such that any two distinct nodes of $S$ are connected by an edge in $G$ ?
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|\geq k\;\wedge\;\forall u,v\in S: (u\neq v\;\Rightarrow\;\{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 greater than the number of nodes, then no such clique exists. Repeated edges and self-loop edges are ignored.

Authors: Carles Creus / Documentation: