# Is SAT with two “opposite” solutions NP-hard?

Here is a variant of the SAT problem in which a satisfying assignment must have additional properties.
Input: A 3-CNF formula $f$ with variables $x_{1\dots k}$.
Output: For an assignment $S$ of $x_{1\dots k}$, let $\overline S$ be defined such that $x_i=true$ in $\overline S$ if and only if $x_i=false$ in $S$. Is there an assignment $S$ such that both $f(S)$ and $f(\overline S)$ hold?

Is this problem still NP-hard?

Examples:

1. $f=(x_1\lor x_2\lor x_3)\land(x_1\lor x_2\lor \neg x_3)\land(x_1\lor \neg x_2\lor x_3)\land(x_1\lor \neg x_2\lor \neg x_3)$
This requires $x_1=true$ in $S$, but then $x_1=false$ in $\overline S$, so $f(S)$ and $f(\overline S)$ cannot simultaneously hold.
2. $f=(x_1\lor x_2\lor x_3)\land(x_1\lor x_2\lor \neg x_3)\land(x_1\lor \neg x_2\lor x_3)$
$S=\{x_1:true,~x_2:false,~x_3:false\}$
$\overline S=\{x_1:false,~x_2:true,~x_3:true\}$
Then both $f(S)$ and $f(\overline S)$ hold.
• This is the Not-all-equal SAT problem (or NAE-SAT), and it is well known to be NP-complete (e.g. The first result in google) – Shaull Jul 12 '15 at 9:08
• NAE-SAT requires each clause to have both a positive and negative assignment, which is a different problem. There could well be a NAE-SAT instance with a unique satisfying assignment, while for this problem there must always be at least two. – Tim Jul 12 '15 at 9:21
• Nope. For every NAE assignment, it's complement is also a NAE assignment. – Shaull Jul 12 '15 at 9:43
• That makes sense, I suppose that answers the question. – Tim Jul 12 '15 at 10:06
• @Shaull, what you're saying is not consistent with the source you're citing. It says: Here the input is a formula in 3-CNF, but the formula is “satisfied” only if there is both a true literal and a false literal in each clause. This is not the same as being asked. For instance, $(z\lor x\lor y)\land(\lnot x\lor y)$, set $y=1$,$z=0$,$x=1$. But $y$ cannot be flipped. – Mikolas Jul 13 '15 at 10:42

Turning my comment to an answer: The problem you describe is known as Not All Equal SAT (NAE-SAT), but is phrased differently. A NAE assignment for a CNF-formula $\phi$ over variables is one where in each clause there is at least one false variable and one true variable.
First, given a 3-CNF formula, we can convert it to a 4-CNF formula by adding a variable $w$ and converting every clause of the form $(x\vee y\vee z)$ to $(x\vee y\vee z\vee w)$.