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).

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.

See also

• Boolean satisfiability problem

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.