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

<p>The reduction is from 1-in-3 SAT with 3 distinct variables per clause:</p>

<ul>
<li>First of all, include all the clauses in the input formula as clauses in the output formula. </li>
<li>Second, introduce three new variables <span class="math-container">$F_1$</span>, <span class="math-container">$F_2$</span>, and <span class="math-container">$F_3$</span> and add the following three clauses to the output formula: <span class="math-container">$(\neg F_1, F_2, F_3)$</span>, <span class="math-container">$(F_1, \neg F_2, F_3)$</span>, and <span class="math-container">$(F_1, F_2, \neg F_3)$</span>. </li>
<li>Finally, for each variable <span class="math-container">$x$</span> in the original formula, introduce a new variable <span class="math-container">$x'$</span>, and add the following two clauses to the output formula: <span class="math-container">$(x, x', F_1)$</span> and <span class="math-container">$(\neg x, \neg x', F_1)$</span>.</li>
</ul>

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

<ol>
<li>Each clause always has three distinct variables.</li>
<li>Each variable occurs in some clause positively and in some clause negatively.</li>
<li>The input formula is equivalent to the output formula.</li>
</ol>

<p>Property 1 is trivial to check. Property 2 is also easy to check: the variables <span class="math-container">$F_1$</span>, <span class="math-container">$F_2$</span>, and <span class="math-container">$F_3$</span> 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.</p>

<p>As for property 3, this is less trivial but still easy. You can easily argue that the only assignment for variables <span class="math-container">$F_1$</span>, <span class="math-container">$F_2$</span>, and <span class="math-container">$F_3$</span> that satisfies each clause from the second bullet point is to make all three <span class="math-container">$F_i$</span>s false. But then assuming a value of false for <span class="math-container">$F_1$</span>, the clauses <span class="math-container">$(x, x', F_1)$</span> and <span class="math-container">$(\neg x, \neg x', F_1)$</span> added in the third bullet point are satisfied if and only if <span class="math-container">$x' = \neg x$</span>. Since there are no other constraints on <span class="math-container">$x'$</span>, 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 <span class="math-container">$x'$</span> to be the negation of the corresponding <span class="math-container">$x$</span> and set each <span class="math-container">$F_i$</span> to false.</p>

CC BY-SA 4.0
2019-01-17T10:39:57.190Z
2019-01-17T10:39:57.190Z
Mikhail Rudoy
<p>The standard problem <strong>1-in-3 SAT</strong> (or XSAT or X3SAT) is: <br>
<strong>Instance</strong>: a CNF formula with every clause containing exactly 3 literals<br>
<strong>Question</strong>: is there a satisfying assignment setting precisely 1 literal per clause true?</p>

<p>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 <em>occur at least once positively and at least once negatively</em>.</p>

<p>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.</p>

CC BY-SA 3.0
2015-07-11T20:01:12.223Z
Can it be reduced to 2 sat?
Joshua Herman
CC BY-SA 3.0
2015-07-12T02:43:09.117Z
hint: for each var $X_i$, add clauses $(X_i\vee \overline X_i \vee W) \wedge (X_i\vee \overline X_i \vee Y)\wedge (X_i\vee \overline X_i \vee Z)$ and, say, $(W \vee Y \vee \overline Z)$.
Neal Young
CC BY-SA 3.0
2015-07-12T07:05:22.750Z
Ha, that works (of course adding also $(\overline W \lor Y\lor Z)\land(W\lor\overline Y \lor Z)$). I'll leave the question open in case anyone can solve it without the ever-so-slightly unsatisfying $X_i\lor\overline X_i$ trick.
Dominik Peters
CC BY-SA 3.0
2015-07-17T22:46:45.883Z
May I encourage you to write up a complete answer to your own question, perhaps based upon Neal young's idea?  (Incidentally, I'm not sure why that is "unsatisfying".  A reduction is a reduction.)
D.W.
CC BY-SA 3.0
2015-07-18T12:15:18.140Z
@D.W. As the 3SAT-reduction I mention in the question shows, 1-in-3 SAT remains hard even if each clause contains 3 distinct _variables_, rather than just 3 distinct literals. Neal's reduction doesn't preserve this qualifier.
Dominik Peters
CC BY-SA 3.0
2015-07-18T15:43:00.393Z
If that special case is the one you really care about, then maybe it makes sense to edit your question to reflect that extra constraint?
D.W.
<cc.complexity-theory><np-hardness><sat>
Does 1-in-3 SAT remain NP-hard even if every variable occurs both positively and negatively?
Dominik Peters
# Does 1-in-3 SAT remain NP-hard even if every variable occurs both positively and negatively?

(Asked by: username_0 on 2015-07-11)

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.

**Tags:** cc.complexity-theory, np-hardness, sat

> **Comments:**
> **username_1**: Can it be reduced to 2 sat?  
> **username_2**: hint: for each var $X_i$, add clauses $(X_i\vee \overline X_i \vee W) \wedge (X_i\vee \overline X_i \vee Y)\wedge (X_i\vee \overline X_i \vee Z)$ and, say, $(W \vee Y \vee \overline Z)$.  
> **username_0**: Ha, that works (of course adding also $(\overline W \lor Y\lor Z)\land(W\lor\overline Y \lor Z)$). I'll leave the question open in case anyone can solve it without the ever-so-slightly unsatisfying $X_i\lor\overline X_i$ trick.  
> **username_3**: May I encourage you to write up a complete answer to your own question, perhaps based upon Neal young's idea?  (Incidentally, I'm not sure why that is "unsatisfying".  A reduction is a reduction.)  
> **username_0**: @username_3 As the 3SAT-reduction I mention in the question shows, 1-in-3 SAT remains hard even if each clause contains 3 distinct _variables_, rather than just 3 distinct literals. Neal's reduction doesn't preserve this qualifier.  
> **username_3**: If that special case is the one you really care about, then maybe it makes sense to edit your question to reflect that extra constraint?  

---

## 1 answers

### Answer by username_4 on 2019-01-17. Score: 2

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.


---

