Exercise 7 | RACSO

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:

Authors: Nil Mamano / Documentation: