Exercise ‹24›:

UNDIRECTED HAMILTONIAN CIRCUIT $\leq$ SAT
Reduce the UNDIRECTED HAMILTONIAN CIRCUIT problem to the SAT problem. These problems are defined as follows:
• UNDIRECTED HAMILTONIAN CIRCUIT: given an undirected graph $G$, is there a cycle that visits each node of $G$ exactly once? In other words, is it possible to order the nodes of $G$ such that there is an edge between each $2$ contiguous nodes and an edge between the last and the first nodes?
More formally, this problem can be defined as the following set:
$\{ G=\langle V,E\rangle \mid V=\{n_1,\ldots,n_k\}\;\wedge\;\forall i\in\{1,\ldots,k\}: \{n_i,n_{(i\text{ mod }k)+1}\}\in E \}$
• 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 {
numnodes: int
edges: array of array [2] of int
adjacents: array of array of int
adjacencymatrix: array of array of int
}

The input is 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 $2$ nodes, no repeated edges, nor self-loop edges.
• 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:
 main { // Write your reduction here... } To be able to submit you need to either log in, register, or become a guest.