## Exercise ‹6›:

SAT $\leq$ 3-DIMENSIONAL MATCHING
Reduce the SAT problem to the 3-DIMENSIONAL MATCHING 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} \}$
• 3-DIMENSIONAL MATCHING: given three finite sets $S_1,S_2,S_3$ and a ternary relation $R$ on those sets, is there a subrelation $S$ of $R$ such that each element of $S_1,S_2,S_3$ occurs exactly once in $S$?
More formally, this problem can be defined as the following set:
$\{ \langle S_1,S_2,S_3,R\rangle \mid S_1,S_2,S_3\text{ finite sets}\;\wedge\;|S_1|=|S_2|=|S_3|\;\wedge\;R\subseteq (S_1\times S_2\times S_3)\;\wedge\;\exists S\subseteq R: (\forall i\in\{1,2,3\}: \forall e\in S_i: \exists!\langle e_1,e_2,e_3\rangle\in S: e_i=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: array of array [3] of string

The output is the list of triplets of the ternary relation $R$: the first position of each triplet corresponds to an element of $S_1$, the second position to an element of $S_2$, and the third position to an element of $S_3$. Each set $S_i$ is implicitly formed by all the elements occurring at the $i$’th position of the triplets.

Note: If the output is an empty relation, then the matching trivially exists. If the sets $S_1,S_2,S_3$ inferred from the relation do not have the same cardinal, then the matching does not exists.
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.