## Exercise ‹7›:

SAT $\leq$ FORMULA-NO-EQUIV
Reduce the SAT problem to the FORMULA-NO-EQUIV 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} \}$
• FORMULA-NO-EQUIV: given two boolean formulas $F_1$ and $F_2$ in conjunctive normal form, are $F_1$ and $F_2$ not logically equivalent? In other words, is there a model $\mathcal{M}$ that satisfies one of $F_1,F_2$ but not the other?
More formally, this problem can be defined as the following set:
$\{ \langle F_1=C_1\wedge\ldots\wedge C_n,\;F_2=C'_1\wedge\ldots\wedge C'_m \rangle \mid \exists \mathcal{M}: \neg((\mathcal{M}\models F_1)\Leftrightarrow(\mathcal{M}\models F_2)) \}$
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 {
F1: array of array of string
F2: array of array of string
}

The output are two lists 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 contains an empty formula, it is considered satisfiable. If the formula has any empty clause, it is considered unsatisfiable.
Authors: Nil Mamano / Documentation:
 main { // Write your reduction here... } To be able to submit you need to either log in, register, or become a guest.