## Exercise ‹8›:

3-SAT $\leq$ 1-in-3-SAT
Reduce the 3-SAT problem to the 1-in-3-SAT problem. These problems are defined as follows:
• 3-SAT: given a boolean formula $F$ in conjunctive normal form where each clause has $3$ literals, 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}\;\wedge\;\forall i\in\{1,\ldots,n\}: |C_i|=3 \}$
• 1-in-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 exactly one true 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 exactly one true literal per clause}\;\wedge\;\forall i\in\{1,\ldots,n\}: |C_i|=3 \}$
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: array of array [3] of string

The output is a list of clauses, where each clause has exactly three literals. 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.
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.