1-in-3-SAT

In computational complexity, one-in-three 3-SAT is an NP-complete variant of the Boolean satisfiability problem.
Given a conjunctive normal form with three literals per clause, the problem is to determine whether there exists a truth assignment to the variables so that each clause has exactly one TRUE literal. In contrast, ordinary 3-SAT requires that every clause has at least one TRUE literal. Formally, a one-in-three 3-SAT problem is given as a generalized conjunctive normal form with all generalized clauses using a ternary operator R that is TRUE just if exactly one of its arguments is. When all the variables of a one-in-three 3-SAT formula have the same literal, the satisfiability problem is called one-in-three monotone 3-SAT.
One-in-three 3-SAT, together with its monotone case, is listed as NP-complete problem "LO4" in the standard reference Computers and Intractability: A Guide to the Theory of NP-Completeness by Michael R. Garey and David S. Johnson. One-in-three 3-SAT was proved to be NP-complete by Thomas Jerome Schaefer as a special case of Schaefer's dichotomy theorem, which asserts that any problem generalizing Boolean satisfiability in a certain way is either in the class P or is NP-complete.

Examples

Here is a satisfiable 1-in-3-SAT instance of 3 variables and 1 clause:
This instance admits 3 solutions:

a=false, b=false, c=false
a=true, b=true, c=false
a=true, b=false, c=true

Here is a unique 1-in-3-SAT instance, that is to say a 1-in-3-SAT instance that admits exactly one solution:
The unique solution is a=true, b=false, c=false, d=false, e=true, f=true, g=true, h=false, i=false
And here is an unsatisfiable 1-in-3-SAT instance:

Here is the truth table that proves that there is no solutions

Reduction from 3-SAT to 1-in-3-SAT

Schaefer gives a construction allowing an easy polynomial-time reduction from 3-SAT to one-in-three 3-SAT. Let "" be a clause in a 3CNF formula. Add six fresh Boolean variables a, b, c, d, e, and f, to be used to simulate this clause and no other. Then the formula R ∧ R ∧ R ∧ R ∧ R is satisfiable by some setting of the fresh variables if and only if at least one of x, y, or z is TRUE, see table. Thus any 3-SAT instance with m clauses and n variables may be converted into an equisatisfiable one-in-three 3-SAT instance with 5m clauses and n + 6m variables.

∨ ∨	R ∧ R ∧ R ∧ R ∧ R	Value
∨ ∨	R ∧ R ∧ R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R ∧ R ∧ R

The result of R is if exactly one of its arguments is TRUE, and otherwise. All 8 combinations of values for x,''y,z'' are examined, one per line. The fresh variables a,...,f can be chosen to satisfy all clauses in all lines except the first, where x ∨ y ∨ z is FALSE.
Another reduction involves only four fresh variables and three clauses: R ∧ R ∧ R, see table. This is not a parsimonious reduction. When x=1, y=0 and z=1, you can have a=1, b=0, c=1 and d=0, but you can also have a=0, b=1, c=0 and d=1.

∨ ∨	R ∧ R ∧ R	Value
∨ ∨	R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R
∨ ∨	R ∧ R ∧ R

Positive 1-in-3-SAT

Positive one-in-three 3-SAT is a specific case where all the literals of the formula are positive. Positive 1-in-3-SAT is NP-complete. A 1-in-3-SAT formula can be reduced in polynomial time to positive 1-in-3-SAT formula by introducing hidden variables that are the negative of the variables appearing with a negative literal. Then some clauses have to be added to force those new variables to be the negative:
is a new variable that is always the negative of and the new variables, and are constants and can be reused for the reductions of the other clauses. For a formula of variables and clauses, the reduced formula has at most variables and clauses but it can be less if we allow constants or the same variable twice in a clause.

Simplification rules

Some rules allow to make the size of an instance smaller in polynomial time. Like other NP-complete problems, if a group of variables doesn't share any clause with the remaining group of variables, so the two groups represent two distinct 1-in-3-SAT instances that can be computed independently. The solutions of the original instance is the cartesian product of the solutions of the two instances and the original instance is unsolveable if at least one sub-instance is unsolveable.
Local analysis can simplify an instance:

A clause including the constant can be safely removed and the remaining literals of the clause are set to.
A clause including twice constant can be safely removed and the remaining literal of the clause is set to.
A clause including one constant can be safely removed and one literal of the clause can be replaced by the opposite of the third literal of the clause.
A clause including twice the same literal can be safely removed, the literal is set to and the third literal to.
A clause including a literal and its opposite can be safely removed and the third literal is set to.

Some rules imply two clauses:

When two clauses share two same variables with the same literals, only one clause is kept and the third literals in the both clauses are equal so one is replaced by the other in the entire instance.
When two clauses share two same variables with opposite literals, we can safely remove the both clauses, replace one variable by the opposite of the other and set the third literals in the both clause to.
When two clauses share two same variables with one opposite and one same literals, we can safely remove the both clauses, set the variable with the same literal to and the third literals can be replaced by the opposite of the variable with the opposite literal.

The following rule is a pattern implying four clauses:
At the first position, two literals are present twice, at the second position, two literals are present twice, and at the third position, one literal is present twice but no clause share two identical literals. It can be simplified this way:
The following rule is a pattern implying a dynamic number of clauses:
We can replace by.
Proof

If x₁=0, so y₁=1 or z₁=1 so x₂=0 so y₂=1 or z₂=1 so x₃=0 so y₃=1 or z₃=1... so x_n−1=0 so y_n−1=1 or z_n−1=1 so x_n=0
If x₁=1, so y₁=z₁=0 so y₂=z₂ so y₃=z₃... so y_n−1=z_n−1 so y_n−1=z_n−1=0 and x_n=1