This is jumping ahead a little, but this is a variant of 3SAT that will be helpful in the future (actually, for the next problem)

**The problem: **Not-All-Equal-3SAT (NAE3SAT). This is problem LO3 in the appendix.

**The description:** Just like 3SAT, except instead of requiring at least one of the literals in each clause to be true, we’re requiring at least one literal to be true* and* at least one literal to be false. So we’re removing the case where all three literals can be true.

Notice that if we have an assignment of variables that is a NAE3SAT solution, then if we negate *all* of the variables, we *still* have a NAE3SAT solution

**The reduction**: From regular 3SAT. We’re given a formula that is a collection of 3-literal clauses. For each clause (x_{1} ∨ x_{2} ∨ x_{3}) we create a new variable c_{i} (for clause i) and add 2 clauses to our NAE3SAT instance:

(x_{1}∨ x_{2} ∨ c_{i}) and (x_{3} ∨ ~c_{i} ∨ F) (Where “F” is the constant value false. We’ll talk more about this later)

The idea is that c_{i} is there to “fix” the clause. If the original clause was satisfiable because of x_{1} or x_{2}, then c_{i} can be false, and its negation can make the second clause true. If the original clause was satisfiable because of x_{3}, we can make c_{i} true. If the original clause had *all three* literals satisfiable, we can make c_{i} false, and become an acceptable NAE3SAT solution.

Note that because the definition of NAE3SAT (and, for that matter, regular 3SAT) is defined in terms of collections of 3 variables, the constant value false we used above isn’t strictly legal. We’ve really just shown “NAE3SAT with some constants replacing variables” is NP-Hard. To show “normal” NAE3SAT is NP-Hard, we need to reduce the fixed constant version into the normal version:

Given an instance of NAE3SAT with fixed constants, we create 2 new variables x_{T} and x_{F}. We replace all instances of the constant value true with x_{T}, and all instances of the constant value false with x_{F}. We also add one additional clause:

(x_{T} ∨ x_{T} ∨ x_{F}).

Note that this new clause is only NAESatisfiable if x_{T} != x_{F}. We can’t directly bind x_{T} to true and x_{F} to false because if you take a NAE3SAT solution and negate all literals, you get another NAE3SAT solution. But because of that, this is NAESatisfiable if and only if the original formula is.

**Difficulty**: It depends on what you give them. If you make them do everything I did above, I’d say it’s an 8. If you let them stop at the NAE3SAT with fixed constants, then maybe a 7.