Does 1-in-3 SAT remain NP-hard even if every variable occurs both positively and negatively?

Question

The standard problem 1-in-3 SAT (or XSAT or X3SAT) is:
Instance: a CNF formula with every clause containing exactly 3 literals
Question: is there a satisfying assignment setting precisely 1 literal per clause true?

The problem is NP-complete and remains hard even if no variable occurs negated. I wonder whether this problem becomes easy or remains hard if each variable is required to occur at least once positively and at least once negatively.

The usual reduction from 3SAT showing that 1-in-3 SAT is hard replaces a clause $(x\lor y \lor z)$ by clauses $(\lnot x \lor a \lor b)$, $(y\lor b\lor c)$, $(\lnot z \lor c \lor d)$ where $a,b,c,d$ are fresh for each clause. Thus, this reduction doesn't help in answering my question. I've had trouble coming up with a gadget showing hardness of this variant, since if exactly 1 literal in a clause is true, then non-symmetrically 2 literals are false. If it turns out to be easy, thinking in terms of partitions of the clause set might do it, but I can't see how.

Answer 1

In a comment, OP expressed interest in a reduction which generated instances with 3 distinct variables per clause. Here's a simple approach:

The reduction is from 1-in-3 SAT with 3 distinct variables per clause:

• First of all, include all the clauses in the input formula as clauses in the output formula.
• Second, introduce three new variables $F_1$, $F_2$, and $F_3$ and add the following three clauses to the output formula: $(\neg F_1, F_2, F_3)$, $(F_1, \neg F_2, F_3)$, and $(F_1, F_2, \neg F_3)$.
• Finally, for each variable $x$ in the original formula, introduce a new variable $x'$, and add the following two clauses to the output formula: $(x, x', F_1)$ and $(\neg x, \neg x', F_1)$.

Let's verify that this reduction does what we want. The following properties are what we want:

1. Each clause always has three distinct variables.
2. Each variable occurs in some clause positively and in some clause negatively.
3. The input formula is equivalent to the output formula.

Property 1 is trivial to check. Property 2 is also easy to check: the variables $F_1$, $F_2$, and $F_3$ each occur both positively and negatively in the clauses added in the second bullet point, while every other variable in the formula occurs both positively and negatively in the clauses added in the third bullet point.

As for property 3, this is less trivial but still easy. You can easily argue that the only assignment for variables $F_1$, $F_2$, and $F_3$ that satisfies each clause from the second bullet point is to make all three $F_i$s false. But then assuming a value of false for $F_1$, the clauses $(x, x', F_1)$ and $(\neg x, \neg x', F_1)$ added in the third bullet point are satisfied if and only if $x' = \neg x$. Since there are no other constraints on $x'$, this means that it is always possible to extend a satisfying assignment for the input formula into a satisfying assignment for the output formula: simply set each $x'$ to be the negation of the corresponding $x$ and set each $F_i$ to false.