Claim: $3SAT \le_p 4NAE $, where reduction $f$ is defined as such: given a 3CNF formula $\varphi$, add to each clause a new literal $z$ (where $z$ is same literal for each clause), and return new formula $f(\varphi)$.
It seemed pretty easy to show that $\varphi\in 3SAT\Rightarrow f(\varphi)\in 4NAE$:
- If $\varphi \in 3SAT$, then every clause in $\varphi$ contains at least one $T$ literal. In $f(\varphi)$, let the added literal $z=F$. Then every clause in $f(\varphi)$ contains at least one $T$ and one $F$ literal, so $f(\varphi)\in 4NAE$.
Here's where I'm confused: At first, I thought that if $\varphi \notin 3SAT \Rightarrow f(\varphi) \notin 4NAE$.
We know $\varphi \notin 3SAT$ iff any non-contradictory assignment of literals has at least one clause with all false values. However, assuming there is no clause in $\varphi$ containing all true literals, then if $f(\varphi)$ adds $z=T$ to each clause, wouldn't $f(\varphi)$ belong to $4NAE$?
On the other hand, I thought of this argument to show that $ f(\varphi)\in 4NAE \Rightarrow \varphi\in 3SAT$:
Suppose $f(\varphi)\in 4NAE$, where $x_i$ represents original literals in $\varphi$ and $z$ is added literal from reduction. Let $Y$ represent a satisfying assigment of $f(\varphi)$.
If $z=F$, then for any clause $(x_1 \vee x_2 \vee x_3 \vee z)$ in $f(\varphi)$, we know that either $x_1$ or $x_2$ or $x_3$ had to be true. Thus, the original clause $(x_1 \vee x_2 \vee x_3)$ in $\varphi$ would evaluate as true, and so $\varphi$ contains satisfiable assignment.
if $z=T$, then for any clause $(x_1 \vee x_2 \vee x_3 \vee z)$ in $f(\varphi)$, we know that either $x_1$ or $x_2$ or $x_3$ had to be false. Now define the assignment $Y '$ to be identical to $Y$ except with every literal negated, and remove all $z$'s. Then $(\bar x_1 \vee \bar x_2 \vee \bar x_3)$ contains at least one true literal. So $Y'$ is a satisfiable assignment of $\varphi $, and $\varphi \in 3SAT$.
Basic logic says if p then q should be equivalent to "if not q then not p". So obviously I'm making some mistakes or assumptions here. I just don't see where.