Complexity of 1-in-3 SAT variant with restrictions on "unique" variables per clause I'm interested in the complexity of a particular variant of 1-in-3 SAT. Assume, as is usual, that clauses are allowed to be of length 1, 2, or 3. Then add the restriction that for any clause of length 3, at least one variable must be "unique," meaning it must appear in no other clause.

Another way to phrase this is, for each clause, at most two variables can be "non-unique" and appear in other clauses.

What is the complexity of this variant of 1-in-3 SAT?
This variant of 1-in-3 SAT is polynomial time solvable. I will try to show this using the fact that 2-CNF-SAT is polynomial time solvable: wikipedia 2-SAT. (There may be better ways or more efficient algorithms for this particular problem) 

Given a special 1-in-3 sat formula $F$, do the following:


Keep the size-1 clauses
Replace any size-2 clause $(\ell_1, \ell_2)$ by formula $(\ell_1\vee \ell_2) \wedge (\neg \ell_1 \vee \neg \ell_2)$
For a size-3 clause $(\ell_1,\ell_2,u)$ where $u$ is unique to this clause: replace it by $(\neg \ell_1 \vee \neg \ell_2)$


It is easy to see that this results in a 2-CNF formula, let's call it $F'$. Use your favorite way to solve 2-SAT to find out whether $F'$ is satisfiable.

Verify that the original 1-in-3 SAT formula is satisfiable, if and only if $F'$ was satisfiable. (If this needs more explanation let me know)