1-in-3-SAT

In computational complexity, one-in-three 3-SAT (also known variously as 1-in-3-SAT and exactly-1 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 (and thus exactly two FALSE literals). 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. ^[1]

Examples

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

R(¬a, b, c)

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:

R(a, b, c) ∧ R(g, h, i) ∧ R(a, d, h) ∧ R(b, d, g) ∧ R(b, e, h) ∧ R(c, f, i)

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 a unsatisfiable 1-in-3-SAT instance:

R(x₁, x₂, x₃) ∧ R(x₅, x₆, x₇) ∧ R(x₁, x₄, x₇) ∧ R(x₂, x₄, x₆) ∧ R(x₃, x₄, x₅)

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

Truth table x1 x2 x3 x4 x5 x6 x7 Result false false false false false false false R(x1, x2, x3) = false false false false false false false true R(x1, x2, x3) = false false false false false false true false R(x1, x2, x3) = false false false false false false true true R(x1, x2, x3) = false false false false false true false false R(x1, x2, x3) = false false false false false true false true R(x1, x2, x3) = false false false false false true true false R(x1, x2, x3) = false false false false false true true true R(x1, x2, x3) = false false false false true false false false R(x1, x2, x3) = false false false false true false false true R(x1, x2, x3) = false false false false true false true false R(x1, x2, x3) = false false false false true false true true R(x1, x2, x3) = false false false false true true false false R(x1, x2, x3) = false false false false true true false true R(x1, x2, x3) = false false false false true true true false R(x1, x2, x3) = false false false false true true true true R(x1, x2, x3) = false false false true false false false false R(x5, x6, x7) = false false false true false false false true R(x2, x4, x6) = false false false true false false true false R(x1, x4, x7) = false false false true false false true true R(x5, x6, x7) = false false false true false true false false R(x1, x4, x7) = false false false true false true false true R(x5, x6, x7) = false false false true false true true false R(x5, x6, x7) = false false false true false true true true R(x5, x6, x7) = false false false true true false false false R(x5, x6, x7) = false false false true true false false true R(x1, x4, x7) = false false false true true false true false R(x2, x4, x6) = false false false true true false true true R(x5, x6, x7) = false false false true true true false false R(x3, x4, x5) = false false false true true true false true R(x5, x6, x7) = false false false true true true true false R(x5, x6, x7) = false false false true true true true true R(x5, x6, x7) = false false true false false false false false R(x5, x6, x7) = false false true false false false false true R(x3, x4, x5) = false false true false false false true false R(x1, x4, x7) = false false true false false false true true R(x5, x6, x7) = false false true false false true false false R(x1, x4, x7) = false false true false false true false true R(x5, x6, x7) = false false true false false true true false R(x5, x6, x7) = false false true false false true true true R(x5, x6, x7) = false false true false true false false false R(x5, x6, x7) = false false true false true false false true R(x1, x4, x7) = false false true false true false true false R(x1, x4, x7) = false false true false true false true true R(x5, x6, x7) = false false true false true true false false R(x2, x4, x6) = false false true false true true false true R(x5, x6, x7) = false false true false true true true false R(x5, x6, x7) = false false true false true true true true R(x5, x6, x7) = false false true true false false false false R(x1, x2, x3) = false false true true false false false true R(x1, x2, x3) = false false true true false false true false R(x1, x2, x3) = false false true true false false true true R(x1, x2, x3) = false false true true false true false false R(x1, x2, x3) = false false true true false true false true R(x1, x2, x3) = false false true true false true true false R(x1, x2, x3) = false false true true false true true true R(x1, x2, x3) = false false true true true false false false R(x1, x2, x3) = false false true true true false false true R(x1, x2, x3) = false false true true true false true false R(x1, x2, x3) = false false true true true false true true R(x1, x2, x3) = false false true true true true false false R(x1, x2, x3) = false false true true true true false true R(x1, x2, x3) = false false true true true true true false R(x1, x2, x3) = false false true true true true true true R(x1, x2, x3) = false true false false false false false false R(x5, x6, x7) = false true false false false false false true R(x3, x4, x5) = false true false false false false true false R(x3, x4, x5) = false true false false false false true true R(x5, x6, x7) = false true false false false true false false R(x2, x4, x6) = false true false false false true false true R(x5, x6, x7) = false true false false false true true false R(x5, x6, x7) = false true false false false true true true R(x5, x6, x7) = false true false false true false false false R(x5, x6, x7) = false true false false true false false true R(x1, x4, x7) = false true false false true false true false R(x1, x4, x7) = false true false false true false true true R(x5, x6, x7) = false true false false true true false false R(x1, x4, x7) = false true false false true true false true R(x5, x6, x7) = false true false false true true true false R(x5, x6, x7) = false true false false true true true true R(x5, x6, x7) = false true false true false false false false R(x1, x2, x3) = false true false true false false false true R(x1, x2, x3) = false true false true false false true false R(x1, x2, x3) = false true false true false false true true R(x1, x2, x3) = false true false true false true false false R(x1, x2, x3) = false true false true false true false true R(x1, x2, x3) = false true false true false true true false R(x1, x2, x3) = false true false true false true true true R(x1, x2, x3) = false true false true true false false false R(x1, x2, x3) = false true false true true false false true R(x1, x2, x3) = false true false true true false true false R(x1, x2, x3) = false true false true true false true true R(x1, x2, x3) = false true false true true true false false R(x1, x2, x3) = false true false true true true false true R(x1, x2, x3) = false true false true true true true false R(x1, x2, x3) = false true false true true true true true R(x1, x2, x3) = false true true false false false false false R(x1, x2, x3) = false true true false false false false true R(x1, x2, x3) = false true true false false false true false R(x1, x2, x3) = false true true false false false true true R(x1, x2, x3) = false true true false false true false false R(x1, x2, x3) = false true true false false true false true R(x1, x2, x3) = false true true false false true true false R(x1, x2, x3) = false true true false false true true true R(x1, x2, x3) = false true true false true false false false R(x1, x2, x3) = false true true false true false false true R(x1, x2, x3) = false true true false true false true false R(x1, x2, x3) = false true true false true false true true R(x1, x2, x3) = false true true false true true false false R(x1, x2, x3) = false true true false true true false true R(x1, x2, x3) = false true true false true true true false R(x1, x2, x3) = false true true false true true true true R(x5, x6, x7) = false true true true false false false false R(x1, x2, x3) = false true true true false false false true R(x1, x2, x3) = false true true true false false true false R(x1, x2, x3) = false true true true false false true true R(x1, x2, x3) = false true true true false true false false R(x1, x2, x3) = false true true true false true false true R(x1, x2, x3) = false true true true false true true false R(x1, x2, x3) = false true true true false true true true R(x1, x2, x3) = false true true true true false false false R(x1, x2, x3) = false true true true true false false true R(x1, x2, x3) = false true true true true false true false R(x1, x2, x3) = false true true true true false true true R(x1, x2, x3) = false true true true true true false false R(x1, x2, x3) = false true true true true true false true R(x1, x2, x3) = false true true true true true true false R(x1, x2, x3) = false true true true true true true true R(x1, x2, x3) = false

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 "(x or y or z)" 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(x,a,d) ∧ R(y,b,d) ∧ R(a,b,e) ∧ R(c,d,f) ∧ R(z,c,FALSE) 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 (below). 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. ^[2]

Schaefer's reduction of a 3-SAT clause x ∨ y ∨ z

x ∨ y ∨ z	R(x, a, d) ∧ R(y, b, d) ∧ R(a, b, e) ∧ R(c, d, f) ∧ R(z, c, 0)	Value
0 ∨ 0 ∨ 0	R(0, a, d) ∧ R(0, b, d) ∧ R(a, b, e) ∧ R(c, d, f) ∧ R(0, c, 0)	FALSE (0)
0 ∨ 0 ∨ 1	R(0, a, d) ∧ R(0, b, d) ∧ R(a, b, e) ∧ R(c, d, f) ∧ R(1, c, 0)	TRUE (1)
0 ∨ 1 ∨ 0	R(0, a, d) ∧ R(1, b, d) ∧ R(a, b, e) ∧ R(c, d, f) ∧ R(0, c, 0)	TRUE (1)
0 ∨ 1 ∨ 1	R(0, a, d) ∧ R(1, b, d) ∧ R(a, b, e) ∧ R(c, d, f) ∧ R(1, c, 0)	TRUE (1)
1 ∨ 0 ∨ 0	R(1, a, d) ∧ R(0, b, d) ∧ R(a, b, e) ∧ R(c, d, f) ∧ R(0, c, 0)	TRUE (1)
1 ∨ 0 ∨ 1	R(1, a, d) ∧ R(0, b, d) ∧ R(a, b, e) ∧ R(c, d, f) ∧ R(1, c, 0)	TRUE (1)
1 ∨ 1 ∨ 0	R(1, a, d) ∧ R(1, b, d) ∧ R(a, b, e) ∧ R(c, d, f) ∧ R(0, c, 0)	TRUE (1)
1 ∨ 1 ∨ 1	R(1, a, d) ∧ R(1, b, d) ∧ R(a, b, e) ∧ R(c, d, f) ∧ R(1, c, 0)	TRUE (1)

The result of R is TRUE (1) if exactly one of its arguments is TRUE, and FALSE (0) 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 (exactly one green argument for each R) in all lines except the first, where x ∨ y ∨ z is FALSE.

Another reduction involves only four fresh variables and three clauses: R(¬x,a,b) ∧ R(b,y,c) ∧ R(c,d,¬z), see table (below). 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.

A simpler reduction with the same properties

x ∨ y ∨ z	R(¬x, a, b) ∧ R(b, y, c) ∧ R(c, d,¬z)	Value
0 ∨ 0 ∨ 0	R(1, a, b) ∧ R(b, 0, c) ∧ R(c, d, 1)	FALSE (0)
0 ∨ 0 ∨ 1	R(1, a, b) ∧ R(b, 0, c) ∧ R(c, d, 0)	TRUE (1)
0 ∨ 1 ∨ 0	R(1, a, b) ∧ R(b, 1, c) ∧ R(c, d, 1)	TRUE (1)
0 ∨ 1 ∨ 1	R(1, a, b) ∧ R(b, 1, c) ∧ R(c, d, 0)	TRUE (1)
1 ∨ 0 ∨ 0	R(0, a, b) ∧ R(b, 0, c) ∧ R(c, d, 1)	TRUE (1)
1 ∨ 0 ∨ 1	R(0, a, b) ∧ R(b, 0, c) ∧ R(c, d, 0)	TRUE (1)
1 ∨ 1 ∨ 0	R(0, a, b) ∧ R(b, 1, c) ∧ R(c, d, 1)	TRUE (1)
1 ∨ 1 ∨ 1	R(0, a, b) ∧ R(b, 1, c) ∧ R(c, d, 0)	TRUE (1)

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:

R(a ∨ b ∨ ¬c) => R(a ∨ b ∨ c') ∧ R(c ∨ c' ∨ alwaysZero) ∧ R(c ∨ c' ∨ alwaysZeroToo) ∧ R(alwaysZero ∨ alwaysZeroToo ∨ alwaysOne)

c' is a new variable that is always the negative of c and the new variables alwaysZero, alwaysZeroToo and alwaysOne are constants and can be reused for the reductions of the other clauses. For a formula of n variables and m clauses, the reduced formula has at most 2n + 3 variables and 7m + 1 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 ^[a] . 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 independantly. 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 1 constant can be safely removed and the remaining literals of the clause are set to 0.
• A clause including twice 0 constant can be safely removed and the remaining literal of the clause is set to 1.
• A clause including one 0 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 0 and the third literal to 1.
• A clause including a literal and its opposite can be safely removed and the third literal is set to 0.

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 0.
• 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 0 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:

R(x₁ ∨ y₁ ∨ z₁) ∧

R(x₁ ∨ y₂ ∨ z₂) ∧

R(x₂ ∨ y₁ ∨ z₃) ∧

R(x₂ ∨ y₂ ∨ z₁)

At the first position (in real world, it may be at any 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:

R(x₁ ∨ y₁ ∨ z₁)

x₁ = x₂

y₁ = y₂

z₁ = z₂= z₃

The following rule is a pattern implying a dynamic number of clauses:

R(x₁ ∨ y₁ ∨ z₁) ∧

R(x₂ ∨ y₁ ∨ z₂) ∧

R(x₂ ∨ y₂ ∨ z₁) ∧

R(x₃ ∨ y₃ ∨ z₂) ∧

R(x₃ ∨ y₂ ∨ z₃) ∧

...

R(x_n-1 ∨ y_n-1 ∨ z_n-2) ∧

R(x_n-1 ∨ y_n-2 ∨ z_n-1) ∧

R(x_n ∨ y_n-1 ∨ z_n-1)

We can replace x_n by x₁.

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

See also

• Boolean satisfiability problem

Notes

1. All the rules can be proved by the table of truth.

References

1. Schaefer, Thomas J. (1978). "The complexity of satisfiability problems" (PDF). Proceedings of the 10th Annual ACM Symposium on Theory of Computing. San Diego, California. pp. 216–226. CiteSeerX   10.1.1.393.8951 . doi:10.1145/800133.804350.
2. Schaefer (1978), p. 222, Lemma 3.5.