Exercise 10 | RACSO

Exercise _‹10_›:

NOT-ALL-EQUAL-3-SAT

\leq

3-COLORABILITY

Reduce the NOT-ALL-EQUAL-3-SAT problem to the 3-COLORABILITY problem. These problems are defined as follows:

NOT-ALL-EQUAL-3-SAT: given a boolean formula $F$ in conjunctive normal form where each clause has $3$ literals, is there a truth assignment to the variables of $F$ such that each clause of $F$ has at least one true literal and one false literal?
More formally, this problem can be defined as the following set:
$\{ F=C_1\wedge\ldots\wedge C_n \mid F\text{ satisfiable with at least one true literal and one false literal per clause}\;\wedge\;\forall i\in\{1,\ldots,n\}: |C_i|=3 \}$
3-COLORABILITY: given an undirected graph $G$ , is $G$ $3$ -colorable? In other words, is there a mapping $M$ from the nodes of $G$ to $\{1,2,3\}$ satisfying $M(u)\neq M(v)$ for each edge $\{u,v\}$ of $G$ ?
More formally, this problem can be defined as the following set:
$\{ G=\langle V,E\rangle \mid \exists M:V\to\{1,2,3\}\text{ total}: \forall \{u,v\}\in E: M(u)\neq M(v) \}$

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

```
in: struct {
      numvars: int
      clauses: array of array [3] of int
    }
```
The input is a boolean formula in conjunctive normal form, where each clause has exactly three literals: 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 exactly three literals, and there are no repeated literals in a clause. Thus, in.numvars is at least $2$ .
```
out: struct {
       edges: array of array [2] of string
       nodes: array of string
     }
```
The output is 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 graph has no nodes, it is colorable. If it has self-loop edges, it is not colorable. Repeated edges are ignored.

Authors: Carles Creus / Documentation: