How do I reduce 3-SAT to a 3-SAT NAE problem?

Question

I am trying to figure out how to reduce a 3SAT problem to a 3SAT NAE (Not All Equal) problem.

Not only that, I also figure out that I am not so sure about the reduction to 3SAT either.

Anyway, how do I go for that?

Since the size of each clause is already the same, I don't have to work on that. But I can't seem to find a way to create an instance I2 of 3SAT-NAE which is accepted iff the 3SAT accepts it.

EXTRA QUESTION: Does SAT (or 3SAT) allow any operation in the clauses? Because I always saw V (or) and never other operations. That confuses me a lot, because if it only allows V, then I don't get the reduction I found; but if it accepts even AND, then I get it.

Answer 1

A more straightforward solution is the following:

for each clause add a new variable ci and perform the following transformation.

$(x1 ∨ x2 ∨ x3) \rightarrow (x1 ∨ x2 ∨ ci) ∧ (x3 ∨ \lnot ci ∨ F)$

Where F is the constant value false.

If $(x1 ∨ x2 ∨ x3)$ has a solution where all literals evaluate to true then set ci to false and $(x1∨ x2 ∨ ci) ∧ (x3 ∨ \lnot ci ∨ F)$ is also satisfied with the added condition of "Not-All-Equal".

If $(x1 ∨ x2 ∨ x3)$ has no solution (all literals evaluate to false) then there is no assignment of ci that can make $(x1∨ x2 ∨ ci) ∧ (x3 ∨ \lnot ci ∨ F)$ true.

If $(x1 ∨ x2 ∨ x3)$ has a solution where not all literals evaluate to true then we can always set ci so that $(x1∨ x2 ∨ ci) ∧ (x3 ∨ \lnot ci ∨ F)$ is satisfied.

some examples for the last case:

• if $x1=x2=t \land x3=f$ set ci=f.
• if $x1=x3=t \land x2=f$ set ci=t.

...