Reduction from the SAT problem to the NAE-SAT problem

I study complexity and computation independently.
I have a problem that I can not solve.

That's the problem:

For the SAT problem, there is a version in which we receive as input phrase $\varphi$ in the form of CNF and we have to decide whether there is a placement in each of the closures $\varphi$ provides at least one literal and does not provide at least one literal. (This version is called NAE-SAT, where NAE is the acronym for Not All Equal).

for example:

• $( x_1 \vee \overline{x_2} \vee x_3 )\wedge (\overline{x_1} \vee \overline{x_2} \vee x_3) \in NAE-SAT$ because for the placement $s(x_1)=T$ , $s(x_2)=T$ and $s(x_3)=T$ it holds that in each clause there is a literal about T and a literal about F, since it will show from the shape: $( T \vee F \vee T )\wedge (F \vee F \vee T )$

• $( x_1 \vee x_2 \vee x_3 )\wedge (\overline{x_1} \vee x_2 \vee x_3) \wedge (\overline{x_1} \vee \overline{x_2} \vee x_3) \wedge (\overline{x_1} \vee x_2 \vee \overline{x_3}) \notin NAE-SAT$. because in every placement for the phrase there will be at least one clause in which all the literals will be provided or all will not be provided, contrary to the requirements of the language.

We would like to show a reduction $ SAT \leq _p NAE-SAT
$. Given phrase $\varphi = c_1 \wedge c_2 \wedge \cdots \wedge c_m$ (from the Boolean variables $x_1 , x_2 , \cdots , x_n $) as an instance for the SAT problem, we will first create the new variables $ y_1 , y_2 , \cdots , y_m , z$. Now, for each clause $C_i = (l_{i,1} \vee \cdots \vee l_{i,k_i})$ (which has $k_i \geq 3$ literals) we construct the clauses: $D_{i,1} = (l_{i,1} \vee \cdots \vee l_{i,k_i-1} \vee y_i) $ and $D_{i,2} = ( \overline{y_i} \vee l_{i,k_i} \vee z)$ . Finally, we will define the whole phrase to be $f(\varphi ) = D_{1,1} \wedge D_{1,2} \wedge D_{2,1} \wedge D_{2,2} \wedge \cdots \wedge D_{m,1} \wedge D_{m,2}$.

The question has 3 sections, which are related to each other, so I can not ask each one separately

Section A

As you correctly spotted, the reduction can be implemented in polynomial time, and the blowup in the formula size is indeed linear.

The reduction is also correct, with the caveat mentioned in item 2.
It's not trivial to show, but we'll go at it slowly.

So first, let's assume we allow this construction also for 2 literals. As for 1 literal clauses -- we can assume those don't exist, since given a formula $\phi$, any 1-literal clause immediately forces a value of one of the variables $x$. So we can start by plugging in this value, and removing the clause and all occurrences of $x$ (more precisely - if $x$ was assigned True, we can remove all clauses containing $x$, and remove $\neg x$ from all other clauses, and vice-versa if $x$ was assigned False).

So now for the main reduction.
We need to show two directions of correctness. First, let's assume $\phi\in SAT$. Then it has a satisfying assignment $\pi$.

We'll construct a NAE-satisfying assignment for $f(\phi)$ (note that it's called an "assignment", not "placement").
Consider some clause $C_i$ of $\phi$. Since $\pi\models \phi$, then at least one literal in $C_i$ is assigned True. If one of the literals in $D_{i,1}$ is assigned True, then we assign $y_i$ to False and $z$ to False, and now both clauses that result from $C_i$ are NAE-satisfied.
Otherwise, if all literals in $D_{i,1}$ are assigned to False, then the remaining literal, which appears in $D_{i,2}$ is assigned to True, so by assigning $y_i$ to be True (and $z$ still False), we get again a NAE-satisfying assignment.

Note that we set $z$ to False globally, as it is a single variable.

So the first direction is correct. For the converse, we start with the following observation: if $\tau$ is a NAE-assignment, then the ``inverse'' assignment is also NAE.
Thus, if $f(\phi)$ has a NAE-assignment, we can assume w.l.o.g. that $z$ is assigned to False (if not, we invert the assignment).
From here we make a similar deduction to the above, to obtain a satisfying assignment for $\phi$. Try it and write if you get stuck.

StackExchange Computer Science Q#142597, answer score: 3